def
Lean.Elab.WF.checkCodomains
(names : Array Lake.Name)
(prefixArgs : Array Lean.Expr)
(arities : Array Nat)
(termArgs : Lean.Elab.WF.TerminationArguments)
:
The termination arguments 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}
(preDefs : Array Lean.Elab.PreDefinition)
(unaryPreDefName : Lake.Name)
(prefixArgs : Array Lean.Expr)
(argsPacker : Lean.Meta.ArgsPacker)
(argType : Lean.Expr)
(termArgs : Lean.Elab.WF.TerminationArguments)
(k : Lean.Expr → Lean.Elab.TermElabM α)
:
If the termArgs 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.