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

Safe Haskell | None

Agda.TypeChecking.Rules.LHS.ProblemRest

Synopsis

- useNamesFromPattern :: [NamedArg Pattern] -> Telescope -> Telescope
- noProblemRest :: Problem -> Bool
- typeFromProblem :: Problem -> Type
- problemFromPats :: [NamedArg Pattern] -> Type -> TCM Problem
- updateProblemRest_ :: Problem -> TCM (Nat, Problem)
- updateProblemRest :: LHSState -> TCM LHSState

# 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