|
Agda.TypeChecking.Positivity |
|
|
Description |
Check that a datatype is strictly positive.
|
|
Synopsis |
|
|
|
Documentation |
|
|
Check that the datatypes in the given mutual block
are strictly positive.
|
|
|
Description of an occurrence.
| Constructors | |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
class ComputeOccurrences a where | Source |
|
| Methods | | The first argument is the items corresponding to the free variables.
|
|
|
|
|
Compute the occurrences in a given definition.
|
|
|
Eta expand a clause to have the given number of variables.
Warning: doesn't update telescope or permutation!
This is used instead of special treatment of lambdas
(which was unsound: issue 121)
|
|
|
|
|
|
|
|
|
|
|
Given an OccursWhere computes the target node and an Edge. The first
argument is the set of names in the current mutual block.
|
|
Produced by Haddock version 2.6.0 |