This module contains

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

structure Lean.Elab.TerminationMeasure : 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 measures (including fixed prefix, in unpacked form) to the termination measure.

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

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

instance Lean.Elab.instInhabitedTerminationMeasure : Inhabited TerminationMeasure

@[reducible, inline]

abbrev Lean.Elab.TerminationMeasures : Type

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

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

Elaborates a TerminationBy to an TerminationMeasure.

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

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

def Lean.Elab.TerminationMeasure.structuralArg (measure : TerminationMeasure) : MetaM Nat

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

Delaborates a TerminationMeasure 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 function's parameters are bound “after the colon”.

@[irreducible]

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