| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Rules.LHS.Split
- splitProblem :: Maybe QName -> Problem -> ListT TCM SplitProblem
Documentation
Arguments
| :: Maybe QName | The definition we are checking at the moment. |
| -> Problem | The current state of the lhs patterns. |
| -> ListT TCM SplitProblem |
Split a problem at the first constructor pattern which is actually of datatype type.
Or, if there is no constructor pattern left and the rest type is a record type and the first rest pattern is a projection pattern, split the rest type.
Implicit patterns should have been inserted.