Agda-2.2.10: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.TypeChecking.Injectivity
Synopsis
reduceHead
::
Term
->
TCM
(
Blocked
Term
)
headSymbol
::
Term
->
TCM
(
Maybe
TermHead
)
checkInjectivity
::
QName
-> [
Clause
] ->
TCM
FunctionInverse
functionInverse
::
Term
->
TCM
InvView
data
InvView
=
Inv
QName
Args
(
Map
TermHead
Clause
)
|
NoInv
useInjectivity
::
Comparison
->
Type
->
Term
->
Term
->
TCM
Constraints
Documentation
reduceHead
::
Term
->
TCM
(
Blocked
Term
)
Source
Reduce simple (single clause) definitions.
headSymbol
::
Term
->
TCM
(
Maybe
TermHead
)
Source
checkInjectivity
::
QName
-> [
Clause
] ->
TCM
FunctionInverse
Source
functionInverse
::
Term
->
TCM
InvView
Source
Argument should be on weak head normal form.
data
InvView
Source
Constructors
Inv
QName
Args
(
Map
TermHead
Clause
)
NoInv
useInjectivity
::
Comparison
->
Type
->
Term
->
Term
->
TCM
Constraints
Source
Produced by
Haddock
version 2.6.1