Agda-2.2.10: 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
polarity
::
HasPolarity
a =>
Nat
-> a ->
TCM
Polarity
Source
Produced by
Haddock
version 2.6.1