Safe Haskell | None |
---|
Agda.TypeChecking.Rules.LHS.ProblemRest
- 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
.
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