Agda.TypeChecking.Polarity
- 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
computePolarity :: QName -> TCM ()Source
sizePolarity :: QName -> TCM [Polarity]Source
Hack for polarity of size indices.
composePol :: Polarity -> Polarity -> PolaritySource
class HasPolarity a whereSource
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) |