Safe Haskell | None |
---|
- 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 -> TelescopeSource
Rename the variables in a telescope using the names from a given pattern
noProblemRest :: Problem -> BoolSource
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 → 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 = [identity-permutation, [A, m]]
problemTel = [A : Set, m : Maybe A]
problemRest =
restPats = [just b]
restType = Case m Bool (Maybe A -> Bool)