Safe Haskell | None |
---|---|

Language | Haskell2010 |

## Synopsis

- useNamesFromPattern :: [NamedArg Pattern] -> Telescope -> Telescope
- useNamesFromProblemEqs :: [ProblemEq] -> Telescope -> TCM Telescope
- useOriginFrom :: (LensOrigin a, LensOrigin b) => [a] -> [b] -> [a]
- noProblemRest :: Problem a -> Bool
- initLHSState :: Telescope -> [ProblemEq] -> [NamedArg Pattern] -> Type -> (LHSState a -> TCM a) -> TCM (LHSState a)
- updateProblemRest :: LHSState a -> TCM (LHSState a)

# Documentation

useNamesFromPattern :: [NamedArg Pattern] -> Telescope -> Telescope Source #

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

If there are not at least as many patterns as entries as in the telescope, the names of the remaining entries in the telescope are unchanged. If there are too many patterns, there should be a type error later.

useOriginFrom :: (LensOrigin a, LensOrigin b) => [a] -> [b] -> [a] Source #

noProblemRest :: Problem a -> Bool Source #

Are there any untyped user patterns left?

:: Telescope | The initial telescope |

-> [ProblemEq] | The problem equations inherited from the parent clause (living in |

-> [NamedArg Pattern] | The user patterns. |

-> Type | The type the user patterns eliminate (living in |

-> (LHSState a -> TCM a) | Continuation for when checking the patterns is complete. |

-> TCM (LHSState a) | The initial LHS state constructed from the user patterns. |

Construct an initial `LHSState`

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:
```

lhsTel = [A : Set, m : Maybe A]
lhsOutPat = [A, "m"]
lhsProblem = Problem [A = _, "just a" = "a"]
["_", "just a"]
["just b"] []
lhsTarget = "Case m Bool (Maybe A -> Bool)"
@