Agda.TypeChecking.Rules.LHS.ProblemRest

Documentation

useNamesFromPattern :: [NamedArg Pattern] -> Telescope -> Telescope

Rename the variables in a telescope using the names from a given pattern

noProblemRest :: Problem -> Bool

Are there any untyped user patterns left?

typeFromProblem :: Problem -> Type

Get the type of clause. Only valid if noProblemRest.

problemFromPats

Arguments

:: [NamedArg Pattern]

The user patterns.

-> Type

The type the user patterns eliminate.

-> TCM Problem

The initial problem constructed from the user patterns.

Construct an initial split Problem from user patterns.

updateProblemRest_ :: Problem -> TCM (Nat, Problem)

Try to move patterns from the problem rest into the problem. Possible if type of problem rest has been updated to a function type.

updateProblemRest :: LHSState -> TCM LHSState