Documentation

Lean.Elab.PreDefinition.WF.Rel

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.TerminationArguments) (k : Lean.ExprLean.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.
    Instances For