Agda.TypeChecking.Polarity

Polarity lattice.

(/\)

neg

composePol

polFromOcc

Auxiliary functions

nextPolarity

purgeNonvariant

Computing the polarity of a symbol.

computePolarity

enablePhantomTypes

dependentPolarity

relevantInIgnoringNonvariant

Turn polarity Nonvariant into relevance UnusedArg

mkUnused

nonvariantToUnusedArg

nonvariantToUnusedArgInDef

nonvariantToUnusedArgInClause

Sized types

sizePolarity

checkSizeIndex

class HasPolarity a

polarity