Agda-2.2.6: 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
)
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.
Produced by
Haddock
version 2.4.2