Agda-2.3.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Infered

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]

type FlexibleVars = [Nat]

data Problem' p

Constructors

Problem |
Fields problemInPat :: [NamedArg Pattern] problemOutPat :: p problemTel :: Telescope

Instances

Monoid p => Monoid (Problem' p) |
Raise (Problem' p) |

data Focus

Constructors

Focus |
Fields 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] focusType :: Type
LitFocus Literal OneHolePatterns Int Type |

data SplitProblem

Constructors

Split ProblemPart [Name] (Arg Focus) (Abs ProblemPart) | the [Name]s give the as-bindings for the focus

data SplitError

Constructors

NothingToSplit |
SplitPanic String |

Instances

Error SplitError |

type ProblemPart = Problem' ()

type Problem = Problem' (Permutation, [Arg Pattern])

The permutation should permute `allHoles` of the patterns to correspond to the abstract patterns in the problem.