Support for termination_by notation

structure Lean.Elab.TerminationBy : Type

A single termination_by clause

• ref : Lean.Syntax
• structural : Bool
• vars : Lean.TSyntaxArray [`ident, `Lean.Parser.Term.hole]
• body : Lean.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 Lean.Elab.TerminationBy

Equations

• Lean.Elab.instInhabitedTerminationBy = { default := { ref := default, structural := default, vars := default, body := default, synthetic := default } }

structure Lean.Elab.DecreasingBy : Type

A single decreasing_by clause

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

instance Lean.Elab.instInhabitedDecreasingBy : Inhabited Lean.Elab.DecreasingBy

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 : Lean.Syntax
• terminationBy?? : Option Lean.Syntax
• terminationBy? : Option Lean.Elab.TerminationBy
• decreasingBy? : Option Lean.Elab.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 argument 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 Lean.Elab.TerminationHints

def Lean.Elab.TerminationHints.none : Lean.Elab.TerminationHints

Equations

• Lean.Elab.TerminationHints.none = { ref := Lean.Syntax.missing, terminationBy?? := none, terminationBy? := none, decreasingBy? := none, extraParams := 0 }

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

Logs warnings when the TerminationHints are unexpectedly present.

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

True if any form of termination hint is present.

Equations

• hints.isNotNone = (hints.terminationBy??.isSome || hints.terminationBy?.isSome || hints.decreasingBy?.isSome)

def Lean.Elab.TerminationHints.rememberExtraParams (headerParams : Nat) (hints : Lean.Elab.TerminationHints) (value : Lean.Expr) : Lean.Elab.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 : Lean.Name) (extraParams : Nat) (tb : Lean.Elab.TerminationBy) : Lean.MetaM Unit

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

Equations

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

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

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

Takes apart a Termination.suffix syntax object