Agda-2.2.6: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.Interaction.MakeCase
Synopsis
findClause
::
MetaId
->
TCM
(
QName
,
Clause
)
makeCase
::
InteractionId
->
Range
->
String
->
TCM
[
Clause
]
prettySplitError
::
SplitError
->
TCM
Doc
makeAbsurdClause
::
QName
->
SplitClause
->
TCM
Clause
makeAbstractClause
::
QName
->
SplitClause
->
TCM
Clause
deBruijnIndex
::
Expr
->
TCM
Nat
Documentation
findClause
::
MetaId
->
TCM
(
QName
,
Clause
)
Source
Find the clause whose right hand side is the given meta. Raises an error if there is no such clause.
makeCase
::
InteractionId
->
Range
->
String
->
TCM
[
Clause
]
Source
prettySplitError
::
SplitError
->
TCM
Doc
Source
makeAbsurdClause
::
QName
->
SplitClause
->
TCM
Clause
Source
makeAbstractClause
::
QName
->
SplitClause
->
TCM
Clause
Source
deBruijnIndex
::
Expr
->
TCM
Nat
Source
Produced by
Haddock
version 2.4.2