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