|
Agda.TypeChecking.Rules.LHS |
|
|
|
Synopsis |
|
|
|
Documentation |
|
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
|
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.
|
|
|
Compute the dot pattern instantiations.
|
|
|
|
|
Check if a problem is solved. That is, if the patterns are all variables.
|
|
noShadowingOfConstructors | Source |
|
:: Clause | The entire clause (used for error reporting).
| -> Problem | | -> TCM () | | 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.
|
|
|
|
Check that a dot pattern matches it's instantiation.
|
|
|
Bind the variables in a left hand side. Precondition: the patterns should
all be VarP, WildP, or ImplicitP and the telescope should have
the same size as the pattern list.
|
|
|
Bind as patterns
|
|
|
Rename the variables in a telescope using the names from a given pattern
|
|
|
|
|
noPatternMatchingOnCodata | Source |
|
|
|
Produced by Haddock version 2.4.2 |