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

Agda.TypeChecking.Rules.LHS.Problem

Synopsis

Documentation

data Problem' p Source

Instances

data SplitProblem Source

Constructors

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

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

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

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