- data DotPatternInst = DPI Expr Term Type
- data AsBinding = AsB Name Term Type
- flexiblePatterns :: [NamedArg Pattern] -> FlexibleVars
- dotPatternInsts :: [NamedArg Pattern] -> Substitution -> [Type] -> [DotPatternInst]
- instantiatePattern :: Substitution -> Permutation -> [Arg Pattern] -> [Arg Pattern]
- isSolvedProblem :: Problem -> Bool
- noShadowingOfConstructors :: Clause -> Problem -> TCM ()
- checkDotPattern :: DotPatternInst -> TCM Constraints
- bindLHSVars :: [NamedArg Pattern] -> Telescope -> TCM a -> TCM a
- bindAsPatterns :: [AsBinding] -> TCM a -> TCM a
- useNamesFromPattern :: [NamedArg Pattern] -> Telescope -> Telescope
- checkLeftHandSide :: Clause -> [NamedArg Pattern] -> Type -> (Telescope -> Telescope -> [Term] -> [String] -> [Arg Pattern] -> Type -> Permutation -> TCM a) -> TCM a
- noPatternMatchingOnCodata :: MonadTCM tcm => [(Bool, Arg Pattern)] -> tcm ()
Documentation
flexiblePatterns :: [NamedArg Pattern] -> 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 -> [Type] -> [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 ConstraintsSource
Check that a dot pattern matches it's instantiation.
bindAsPatterns :: [AsBinding] -> TCM a -> TCM aSource
Bind as patterns
useNamesFromPattern :: [NamedArg Pattern] -> Telescope -> TelescopeSource
Rename the variables in a telescope using the names from a given pattern