| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 Arity | Source

computePolarity :: QName -> TCM () | Source

sizePolarity :: QName -> TCM [Polarity] | Source

Hack for polarity of size indices.

checkSizeIndex :: Nat -> Nat -> Type -> TCM Bool | Source

(/\) :: Polarity -> Polarity -> Polarity | Source

neg :: Polarity -> Polarity | Source

composePol :: Polarity -> Polarity -> Polarity | Source

class HasPolarity a where | Source

Methods

polarities :: Nat -> a -> TCM [Polarity] | Source

Instances

HasPolarity Type
HasPolarity Term
HasPolarity a => HasPolarity ([] a)
HasPolarity a => HasPolarity (Arg a)
HasPolarity a => HasPolarity (Abs a)
(HasPolarity a, HasPolarity b) => HasPolarity ((,) a b)

polarity :: HasPolarity a => Nat -> a -> TCM Polarity | Source

Produced by Haddock version 2.4.2