Safe Haskell | None |
---|---|
Language | Haskell98 |
- useNamesFromPattern :: [NamedArg Pattern] -> Telescope -> Telescope
- noProblemRest :: Problem -> Bool
- problemFromPats :: [NamedArg Pattern] -> Type -> TCM Problem
- updateProblemRest_ :: Problem -> TCM (Nat, Problem)
- updateProblemRest :: LHSState -> TCM LHSState
Documentation
useNamesFromPattern :: [NamedArg Pattern] -> Telescope -> Telescope Source #
Rename the variables in a telescope using the names from a given pattern
noProblemRest :: Problem -> Bool Source #
Are there any untyped user patterns left?
:: [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.
Example:
@
Case : {A : Set} → Maybe A → Set → Set → Set Case nothing B C = B Case (just _) B C = C
sample : {A : Set} (m : Maybe A) → Case m Bool (Maybe A → Bool)
sample (just a) (just b) = true
sample (just a) nothing = false
sample nothing = true
The problem generated for the first clause of
sample
with patterns
just a, just b would be:
problemInPat = ["_", "just a"]
problemOutPat = [A, "m"]
problemTel = [A : Set, m : Maybe A]
problemRest =
restPats = ["just b"]
restType = "Case m Bool (Maybe A -> Bool)"
@