Agda.TypeChecking.Positivity
type Graph n e
checkStrictlyPositive
getDefArity
data OccursWhere
data Where
(>*<)
data Item
type Occurrences
data OccurrencesBuilder
data OccurrencesBuilder'
emptyOB
(>+<)
preprocess
data OccursWheres
flatten
data OccEnv
type OccM
withExtendedOccEnv
getOccurrences
class ComputeOccurrences a
computeOccurrences
computeOccurrences'
etaExpandClause
data Node
data Edge
buildOccurrenceGraph
computeEdges