|
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 |
|
|
|
Documentation |
|
|
Get a list of all the datatypes that look like nats. The [QName] is on the
form [zeroConstr, sucConstr]
|
|
|
Count the number of relevant arguments
|
|
|
Check if argument n is recursive
|
|
|
|
Produced by Haddock version 2.6.1 |