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