Agda-2.2.10: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.TypeChecking.Rules.LHS.Split
Synopsis
asView
::
Pattern
-> ([
Name
],
Pattern
)
expandLitPattern
::
NamedArg
Pattern
->
TCM
(
NamedArg
Pattern
)
splitProblem
::
Problem
->
TCM
(
Either
SplitError
SplitProblem
)
wellFormedIndices
::
MonadTCM
tcm => [
Arg
Term
] -> [
Arg
Term
] -> tcm
()
Documentation
asView
::
Pattern
-> ([
Name
],
Pattern
)
Source
TODO: move to Agda.Syntax.Abstract.View
expandLitPattern
::
NamedArg
Pattern
->
TCM
(
NamedArg
Pattern
)
Source
TODO: move somewhere else
splitProblem
::
Problem
->
TCM
(
Either
SplitError
SplitProblem
)
Source
Split a problem at the first constructor of datatype type. Implicit patterns should have been inserted.
wellFormedIndices
Source
::
MonadTCM
tcm
=> [
Arg
Term
]
Parameters.
-> [
Arg
Term
]
Indices.
-> tcm
()
Checks that the indices are constructors applied to distinct variables which do not occur free in the parameters.
Produced by
Haddock
version 2.6.1