Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Compiler.Epic.NatDetection
Description
Detect if a datatype could be represented as a primitive integer. If it has one constructor with no arguments and one with a recursive argument this is true. This is done using IrrFilters which filter out forced arguments, so for example Fin becomes primitive.
Synopsis
getNatish :: MonadTCM m => Compile m [(IrrFilter, [QName])]
nrRel :: IrrFilter -> Integer
isRec :: Int -> Type -> QName -> Bool
argIsDef :: Type -> QName -> Bool
Documentation
getNatish :: MonadTCM m => Compile m [(IrrFilter, [QName])]Source
Get a list of all the datatypes that look like nats. The [QName] is on the form [zeroConstr, sucConstr]
nrRel :: IrrFilter -> IntegerSource
Count the number of relevant arguments
isRec :: Int -> Type -> QName -> BoolSource
Check if argument n is recursive
argIsDef :: Type -> QName -> BoolSource
Produced by Haddock version 2.6.1