def
Lean.Elab.WF.checkCodomains
(names : Array Name)
(prefixArgs : Array Expr)
(arities : Array Nat)
(termMeasures : TerminationMeasures)
:
The termination measures must not depend on the varying parameters of the function, and in a mutual clique, they must be the same for all functions.
This ensures the preconditions for ArgsPacker.uncurryND.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Elab.WF.elabWFRel
{α : Type}
(declNames : Array Name)
(unaryPreDefName : Name)
(prefixArgs : Array Expr)
(argsPacker : Meta.ArgsPacker)
(argType : Expr)
(termMeasures : TerminationMeasures)
(k : Expr → TermElabM α)
:
If the termMeasures map the packed argument argType to β, then this function passes to the
continuation a value of type WellFoundedRelation argType that is derived from the instance
for WellFoundedRelation β using invImage.
Equations
- One or more equations did not get rendered due to their size.