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

Agda.TypeChecking.Rules.LHS.Problem

Synopsis

Documentation

type FlexibleVars = [Nat]

data Problem' p

Instances

data SplitProblem

Constructors

Split ProblemPart [Name] (Arg Focus) (Abs ProblemPart)

the [Name]s give the as-bindings for the focus

data SplitError

Instances

Error SplitError 

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

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