Agda.TypeChecking.Polarity

Polarity lattice.

(/\)

neg

composePol

polFromOcc

Auxiliary functions

nextPolarity

purgeNonvariant

polarityFromPositivity

Computing the polarity of a symbol.

computePolarity

enablePhantomTypes

dependentPolarity

relevantInIgnoringNonvariant

Sized types

sizePolarity

checkSizeIndex

class HasPolarity a

polarity