Agda-2.2.6: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.TypeChecking.Rules.LHS.Problem
Synopsis
type
Substitution
= [
Maybe
Term
]
type
FlexibleVars
= [
Nat
]
data
Problem'
p =
Problem
{
problemInPat
:: [
NamedArg
Pattern
]
problemOutPat
:: p
problemTel
::
Telescope
}
data
Focus
=
Focus
{
focusCon
::
QName
focusConArgs
:: [
NamedArg
Pattern
]
focusRange
::
Range
focusOutPat
::
OneHolePatterns
focusHoleIx
::
Int
focusDatatype
::
QName
focusParams
:: [
Arg
Term
]
focusIndices
:: [
Arg
Term
]
}
|
LitFocus
Literal
OneHolePatterns
Int
Type
data
SplitProblem
=
Split
ProblemPart
[
Name
] (
Arg
Focus
) (
Abs
ProblemPart
)
data
SplitError
=
NothingToSplit
|
SplitPanic
String
type
ProblemPart
=
Problem'
()
type
Problem
=
Problem'
(
Permutation
, [
Arg
Pattern
])
Documentation
type
Substitution
= [
Maybe
Term
]
Source
type
FlexibleVars
= [
Nat
]
Source
data
Problem'
p
Source
Constructors
Problem
problemInPat
:: [
NamedArg
Pattern
]
problemOutPat
:: p
problemTel
::
Telescope
data
Focus
Source
Constructors
Focus
focusCon
::
QName
focusConArgs
:: [
NamedArg
Pattern
]
focusRange
::
Range
focusOutPat
::
OneHolePatterns
focusHoleIx
::
Int
index of focused variable in the out patterns
focusDatatype
::
QName
focusParams
:: [
Arg
Term
]
focusIndices
:: [
Arg
Term
]
LitFocus
Literal
OneHolePatterns
Int
Type
data
SplitProblem
Source
Constructors
Split
ProblemPart
[
Name
] (
Arg
Focus
) (
Abs
ProblemPart
)
the [Name]s give the as-bindings for the focus
data
SplitError
Source
Constructors
NothingToSplit
SplitPanic
String
type
ProblemPart
=
Problem'
()
Source
type
Problem
=
Problem'
(
Permutation
, [
Arg
Pattern
])
Source
The permutation should permute
allHoles
of the patterns to correspond to the abstract patterns in the problem.
Produced by
Haddock
version 2.6.0