Check that a datatype is strictly positive.
- checkStrictlyPositive :: MutualId -> TCM ()
- data OccursWhere
- (>*<) :: OccursWhere -> OccursWhere -> OccursWhere
- data Item
- type Occurrences = Map Item [OccursWhere]
- (>+<) :: Occurrences -> Occurrences -> Occurrences
- concatOccurs :: [Occurrences] -> Occurrences
- occursAs :: (OccursWhere -> OccursWhere) -> Occurrences -> Occurrences
- here :: Item -> Occurrences
- class ComputeOccurrences a where
- computeOccurrences :: QName -> TCM Occurrences
- etaExpandClause :: Nat -> Clause -> Clause
- data Node
- data Edge = Edge Occurrence OccursWhere
- buildOccurrenceGraph :: Set QName -> TCM (Graph Node Edge)
- computeEdge :: Set QName -> OccursWhere -> TCM (Node, Edge)
Check that the datatypes in the given mutual block are strictly positive.
Description of an occurrence.
|DefArg QName Nat OccursWhere|
in the nth argument of a define constant
as an argument to a bound variable
as an argument of a metavariable
|ConArgType QName OccursWhere|
in the type of a constructor
|InClause Nat OccursWhere|
in the nth clause of a defined function
|InDefOf QName OccursWhere|
in the definition of a constant
an unknown position (treated as negative)
The first argument is the items corresponding to the free variables.
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)