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

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) |

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.