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

Equations

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

@[reducible, inline]

abbrev Lean.Elab.TerminationMeasures : Type

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

Equations

• Lean.Elab.TerminationMeasures = Array Lean.Elab.TerminationMeasure

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.

Equations

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

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

Equations

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

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

Equations

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

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”.

Equations

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

@[irreducible]

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

Equations

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