Safe Haskell | None |
---|

- flexiblePatterns :: [NamedArg Pattern] -> TCM FlexibleVars
- dotPatternInsts :: [NamedArg Pattern] -> Substitution -> [Dom Type] -> TCM [DotPatternInst]
- instantiatePattern :: Substitution -> Permutation -> [Arg Pattern] -> [Arg Pattern]
- isSolvedProblem :: Problem -> Bool
- noShadowingOfConstructors :: (Maybe r -> Call) -> Problem -> TCM ()
- checkDotPattern :: DotPatternInst -> TCM ()
- bindLHSVars :: [NamedArg Pattern] -> Telescope -> TCM a -> TCM a
- bindAsPatterns :: [AsBinding] -> TCM a -> TCM a
- checkLeftHandSide :: (Maybe r -> Call) -> [NamedArg Pattern] -> Type -> (Maybe Telescope -> Telescope -> Substitution -> [String] -> [Arg Pattern] -> Type -> Permutation -> TCM a) -> TCM a
- noPatternMatchingOnCodata :: [Arg Pattern] -> TCM ()

# Documentation

flexiblePatterns :: [NamedArg Pattern] -> TCM FlexibleVarsSource

Compute the set of flexible patterns in a list of patterns. The result is the deBruijn indices of the flexible patterns. A pattern is flexible if it is dotted or implicit.

dotPatternInsts :: [NamedArg Pattern] -> Substitution -> [Dom Type] -> TCM [DotPatternInst]Source

Compute the dot pattern instantiations.

instantiatePattern :: Substitution -> Permutation -> [Arg Pattern] -> [Arg Pattern]Source

isSolvedProblem :: Problem -> BoolSource

Check if a problem is solved. That is, if the patterns are all variables.

noShadowingOfConstructorsSource

For each user-defined pattern variable in the `Problem`

, check
that the corresponding data type (if any) does not contain a
constructor of the same name (which is not in scope); this
"shadowing" could indicate an error, and is not allowed.

Precondition: The problem has to be solved.

checkDotPattern :: DotPatternInst -> TCM ()Source

Check that a dot pattern matches it's instantiation.

bindAsPatterns :: [AsBinding] -> TCM a -> TCM aSource

Bind as patterns

:: (Maybe r -> Call) | Trace, e.g. |

-> [NamedArg Pattern] | The patterns. |

-> Type | The expected type |

-> (Maybe Telescope -> Telescope -> Substitution -> [String] -> [Arg Pattern] -> Type -> Permutation -> TCM a) | Continuation. |

-> TCM a |

Check a LHS. Main function.

noPatternMatchingOnCodata :: [Arg Pattern] -> TCM ()Source