Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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]
focusType :: Type
}
| 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 :: Intindex of focused variable in the out patterns
focusDatatype :: QName
focusParams :: [Arg Term]
focusIndices :: [Arg Term]
focusType :: Type
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.1