Agda-2.2.10: A dependently typed functional programming language and proof assistant

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

computePolarity :: QName -> TCM ()

sizePolarity :: QName -> TCM [Polarity]

Hack for polarity of size indices.

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

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

neg :: Polarity -> Polarity

composePol :: Polarity -> Polarity -> Polarity

class HasPolarity a where

Methods

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

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