|
Agda.TypeChecking.Rules.LHS.Unify |
|
|
|
Synopsis |
|
|
|
Documentation |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Includes flexible occurrences, metas need to be solved. TODO: relax?
TODO: later solutions may remove flexible occurences
|
|
|
|
|
|
|
Apply the current substitution on a term and reduce to weak head normal form.
|
|
|
Take a substitution and ensure that no variables from the domain appear
in the targets. The context of the targets is not changed.
TODO: can this be expressed using makeSubstitution and substs?
|
|
|
|
|
|
Unify indices.
|
|
|
|
|
:: MonadTCM tcm | | => QName | Constructor name.
| -> Type | | -> tcm Type | | Given the type of a constructor application the corresponding
data or record type, applied to its parameters (extracted from the
given type), is returned.
Precondition: The type has to correspond to an application of the
given constructor.
|
|
|
Produced by Haddock version 2.6.1 |