def Lean.Elab.WF.checkCodomains (names : Array Lake.Name) (prefixArgs : Array Lean.Expr) (arities : Array Nat) (termArgs : Lean.Elab.TerminationArguments) : Lean.Elab.TermElabM Lean.Expr

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.

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.TerminationArguments) (k : Lean.Expr → Lean.Elab.TermElabM α) : 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.