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