Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Polarity
Synopsis
getArity :: QName -> TCM Arity
computePolarity :: QName -> TCM ()
sizePolarity :: QName -> TCM [Polarity]
checkSizeIndex :: Nat -> Nat -> Type -> TCM Bool
(/\) :: Polarity -> Polarity -> Polarity
neg :: Polarity -> Polarity
composePol :: Polarity -> Polarity -> Polarity
class HasPolarity a where
polarities :: Nat -> a -> TCM [Polarity]
polarity :: HasPolarity a => Nat -> a -> TCM Polarity
Documentation
getArity :: QName -> TCM AritySource
computePolarity :: QName -> TCM ()Source
sizePolarity :: QName -> TCM [Polarity]Source
Hack for polarity of size indices.
checkSizeIndex :: Nat -> Nat -> Type -> TCM BoolSource
(/\) :: Polarity -> Polarity -> PolaritySource
neg :: Polarity -> PolaritySource
composePol :: Polarity -> Polarity -> PolaritySource
class HasPolarity a whereSource
Methods
polarities :: Nat -> a -> TCM [Polarity]Source
show/hide Instances
polarity :: HasPolarity a => Nat -> a -> TCM PolaritySource
Produced by Haddock version 2.4.2