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.

def Lean.Elab.TerminationArgument.elab (funName : Lean.Name) (type : Lean.Expr) (arity 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.

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

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

def Lean.Elab.TerminationArgument.delab (arity 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)