Agda.TypeChecking.MetaVars.Occurs
modifyOccursCheckDefs
initOccursCheck
defNeedsChecking
tallyDef
data OccursCtx
data UnfoldStrategy
defArgs
unfold
leaveTop
weakly
strongly
patternViolation'
abort
type Vars
goIrrelevant
allowedVar
takeRelevant
liftUnderAbs
class Occurs t
occursCheck
prune
hasBadRigid
isNeutral
rigidVarsNotContainedIn
class FoldRigid a
data PruneResult
killArgs
killedType
performKill