Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




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

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

noProblemRest :: Problem -> BoolSource

Are there any untyped user patterns left?

typeFromProblem :: Problem -> TypeSource

Get the type of clause. Only valid if noProblemRest.



:: [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)Source

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