Agda-2.2.6: A dependently typed functional programming language and proof assistant

Agda.Compiler.Agate.Classify

Description

Classify type familes and constants TODO: optimize by getting rid of !'s

Documentation

allM :: Monad m => (a -> m Bool) -> [a] -> m Bool Source

andM :: Monad m => m Bool -> m Bool -> m Bool Source

enumTypeFamilies :: Map QName Definition -> TCM [QName]Source

enumCompilableTypeFamilies :: Map QName Definition -> TCM [QName]Source

enumOptimizableConstants :: Map QName Definition -> [QName] -> TCM [QName]Source

computeGreatestFixedPoint :: ([QName] -> QName -> TCM Bool) -> [QName] -> TCM [QName]Source

computeLeastFixedPoint :: ([QName] -> QName -> TCM Bool) -> [QName] -> TCM [QName]Source