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 -> Integer

Source

Count the number of relevant arguments

isRec :: Int -> Type -> QName -> Bool

Source

Check if argument n is recursive

argIsDef :: Type -> QName -> Bool

Source

Produced by Haddock version 2.6.1