This module contains

• the data type TerminationArgument, the elaborated form of a TerminationBy clause,
• the TerminationArguments type for a clique, and
• elaboration and deelaboration functions.

structure Lean.Elab.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.

If structural := Bool, then the fn is a lambda picking out exactly one argument.

• ref : Lean.Syntax
• structural : Bool
• fn : Lean.Expr

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

Equations

• Lean.Elab.instInhabitedTerminationArgument = { default := { ref := default, structural := default, fn := default } }

@[reducible, inline]

abbrev Lean.Elab.TerminationArguments : Type

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

Equations

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

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

Elaborates a TerminationBy to an TerminationArgument.

• type is the full type of the original recursive function, including fixed prefix.
• hint : TerminationBy is the syntactic TerminationBy.

Equations

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

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

Equations

• Lean.Elab.TerminationArgument.elab.parameters 1 = (Lean.MessageData.ofFormat ∘ Lean.format) "one parameter"
• Lean.Elab.TerminationArgument.elab.parameters x = Lean.toMessageData "" ++ Lean.toMessageData x ++ Lean.toMessageData " parameters"

def Lean.Elab.TerminationArgument.structuralArg (termArg : Lean.Elab.TerminationArgument) : Lean.MetaM Nat

Equations

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

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

Delaborates a TerminationArgument back to a TerminationHint, e.g. for termination_by?.

This needs extra information:

• arity is the value arity of the recursive function
• extraParams indicates how many of the functions arguments are bound “after the colon”.

Equations

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

@[irreducible]

def Lean.Elab.TerminationArgument.delab.go (termArg : Lean.Elab.TerminationArgument) : Nat → Lean.TSyntaxArray `ident → Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax `Lean.Parser.Termination.terminationBy)

Equations

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