Agda.TypeChecking.Positivity
type Graph n e
checkStrictlyPositive
getDefArity
data OccursWhere
(>*<)
data Item
type Occurrences
(>+<)
concatOccurs
occursAs
here
onlyVarsUpTo
data OccEnv
type OccM
withExtendedOccEnv
getOccurrences
class ComputeOccurrences a
computeOccurrences
etaExpandClause
data Node
data Edge
buildOccurrenceGraph
computeEdge