Safe Haskell | Safe-Infered |
---|
- 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
- = Focus {
- data SplitProblem = Split ProblemPart [Name] (Arg Focus) (Abs ProblemPart)
- data SplitError
- type ProblemPart = Problem' ()
- type Problem = Problem' (Permutation, [Arg Pattern])
Documentation
type Substitution = [Maybe Term]Source
type FlexibleVars = [Nat]Source
Problem | |
|
Focus | |
| |
LitFocus Literal OneHolePatterns Int Type |
data SplitProblem Source
Split ProblemPart [Name] (Arg Focus) (Abs ProblemPart) | the [Name]s give the as-bindings for the focus |
type ProblemPart = Problem' ()Source