This module contains the data type TerminationArgument, the elaborated form of a TerminationBy clause, the TerminationArguments type for a clique and the elaboration functions.

structure Lean.Elab.WF.TerminationArgument : Type

Elaborated form for a termination_by clause.

The fn has the same (value) arity as the recursive functions (stored in arity), and maps its arguments (including fixed prefix, in unpacked form) to the termination argument.

• ref : Lean.Syntax
• arity : Nat
• extraParams : Nat
• fn : Lean.Expr

instance Lean.Elab.WF.instInhabitedTerminationArgument : Inhabited Lean.Elab.WF.TerminationArgument

Equations

• Lean.Elab.WF.instInhabitedTerminationArgument = { default := { ref := default, arity := default, extraParams := default, fn := default } }

@[reducible, inline]

abbrev Lean.Elab.WF.TerminationArguments : Type

A complete set of TerminationArguments, as applicable to a single clique.

Equations

• Lean.Elab.WF.TerminationArguments = Array Lean.Elab.WF.TerminationArgument

def Lean.Elab.WF.TerminationArgument.elab (funName : Lake.Name) (type : Lean.Expr) (arity : Nat) (extraParams : Nat) (hint : Lean.Elab.WF.TerminationBy) : Lean.Elab.TermElabM Lean.Elab.WF.TerminationArgument

Elaborates a TerminationBy to an TerminationArgument.

• type is the full type of the original recursive function, including fixed prefix.
• arity is the value arity of the recursive function; the termination argument cannot take more.
• extraParams is the the number of parameters the function has after the colon; together with arity indicates how many parameters of the function are before the colon and thus in scope.
• hint : TerminationBy is the syntactic TerminationBy.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.WF.TerminationArgument.elab.parameters : Nat → Lean.MessageData

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.WF.TerminationArgument.delab (termArg : Lean.Elab.WF.TerminationArgument) : Lean.MetaM (Lean.TSyntax `Lean.Parser.Termination.terminationBy)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.WF.TerminationArgument.delab.go : Nat → Lean.TSyntaxArray [`ident, `Lean.Parser.Term.hole] → Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax `Lean.Parser.Termination.terminationBy)

Equations

• One or more equations did not get rendered due to their size.