Support for termination_by notation

structure Lean.Elab.TerminationBy : Type

A single termination_by clause

• ref : Syntax
• structural : Bool
• vars : TSyntaxArray [`ident, `Lean.Parser.Term.hole]
• body : Term
• synthetic : Bool

  If synthetic := true, then this termination_by clause was generated by GuessLex, and vars refers to all parameters of the function, not just the “extra parameters”. Cf. Lean.Elab.WF.unpackUnary

instance Lean.Elab.instInhabitedTerminationBy : Inhabited TerminationBy

structure Lean.Elab.DecreasingBy : Type

A single decreasing_by clause

• ref : Syntax
• tactic : TSyntax `Lean.Parser.Tactic.tacticSeq

instance Lean.Elab.instInhabitedDecreasingBy : Inhabited DecreasingBy

inductive Lean.Elab.PartialFixpointType : Type

• partialFixpoint : PartialFixpointType
• greatestFixpoint : PartialFixpointType
• leastFixpoint : PartialFixpointType

instance Lean.Elab.instInhabitedPartialFixpointType : Inhabited PartialFixpointType

structure Lean.Elab.PartialFixpoint : Type

A single partial_fixpoint, greatest_fixpoint or least_fixpoint clause

• ref : Syntax
• term? : Option Term
• fixpointType : PartialFixpointType

instance Lean.Elab.instInhabitedPartialFixpoint : Inhabited PartialFixpoint

structure Lean.Elab.TerminationHints : Type

The termination annotations for a single function. For decreasing_by, we store the whole decreasing_by tacticSeq expression, as this is what Term.runTactic expects.

• ref : Syntax
• terminationBy?? : Option Syntax
• terminationBy? : Option TerminationBy
• partialFixpoint? : Option PartialFixpoint
• decreasingBy? : Option DecreasingBy
• extraParams : Nat

  Here we record the number of parameters past the :. It is set by TerminationHints.rememberExtraParams and used as follows:

  • When we guess the termination measure in GuessLex and want to print it in surface-syntax compatible form.
  • If there are fewer variables in the termination_by annotation than there are extra parameters, we know which parameters they should apply to (TerminationBy.checkVars).

instance Lean.Elab.instInhabitedTerminationHints : Inhabited TerminationHints

def Lean.Elab.isLeast : PartialFixpointType → Bool

def Lean.Elab.isGreatest : PartialFixpointType → Bool

def Lean.Elab.isPartial : PartialFixpointType → Bool

def Lean.Elab.isLatticeTheoretic (p : PartialFixpointType) : Bool

def Lean.Elab.TerminationHints.none : TerminationHints

def Lean.Elab.TerminationHints.ensureNone (hints : TerminationHints) (reason : String) : CoreM Unit

Logs warnings when the TerminationHints are unexpectedly present.

def Lean.Elab.TerminationHints.isNotNone (hints : TerminationHints) : Bool

True if any form of termination hint is present.

def Lean.Elab.TerminationHints.rememberExtraParams (headerParams : Nat) (hints : TerminationHints) (value : Expr) : TerminationHints

Remembers extraParams for later use. Needs to happen early enough where we still know how many parameters came from the function header (headerParams).

def Lean.Elab.TerminationBy.checkVars (funName : Name) (extraParams : Nat) (tb : TerminationBy) : MetaM Unit

Checks that termination_by binds at most as many variables are present in the outermost lambda of value, and throws appropriate errors.

def Lean.Elab.TerminationBy.checkVars.parameters : Nat → MessageData

def Lean.Elab.elabTerminationHints {m : Type → Type} [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Termination.suffix) : m TerminationHints

Takes apart a Termination.suffix syntax object