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

Instances

Monoid p => Monoid (Problem' p)

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 |

Instances

Error SplitError

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.4.2