|
Agda.TypeChecking.Rules.Data |
|
|
|
|
|
Synopsis |
|
|
|
|
Datatypes
|
|
|
Type check a datatype definition. Assumes that the type has already been
checked.
|
|
|
Type check a constructor declaration. Checks that the constructor targets
the datatype and that it fits inside the declared sort.
|
|
|
Bind the parameters of a datatype. The bindings should be domain free.
|
|
|
Check that the arguments to a constructor fits inside the sort of the datatype.
The first argument is the type of the constructor.
|
|
|
Check that a type constructs something of the given datatype. The first
argument is the number of parameters to the datatype.
TODO: what if there's a meta here?
|
|
|
Force a type to be a specific datatype.
|
|
|
Is the type coinductive? Returns Nothing if the answer cannot
be determined.
|
|
Produced by Haddock version 2.6.1 |