Support for termination_by notation

structure Lean.Elab.WF.TerminationBy : Type

A single termination_by clause

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

instance Lean.Elab.WF.instInhabitedTerminationBy : Inhabited Lean.Elab.WF.TerminationBy

Equations

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

def Lean.Elab.WF.TerminationBy.unexpand (wf : Lean.Elab.WF.TerminationBy) : Lean.MetaM Lean.Syntax

Equations

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

@[inline, reducible]

abbrev Lean.Elab.WF.TerminationWF : Type

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

Equations

• Lean.Elab.WF.TerminationWF = Array Lean.Elab.WF.TerminationBy

structure Lean.Elab.WF.DecreasingBy : Type

A single decreasing_by clause

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

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

Equations

• Lean.Elab.WF.instInhabitedDecreasingBy = { default := { ref := default, tactic := default } }

structure Lean.Elab.WF.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
• termination_by? : Option Lean.Elab.WF.TerminationBy
• decreasing_by? : Option Lean.Elab.WF.DecreasingBy
• extraParams : Nat

  Here we record the number of parameters past the :. This is

  • GuessLex when there is no termination_by annotation, so that we can print the guessed order in the right form.
  • If there are fewer variables in the termination_by annotation than there are extra parameters, we know which parameters they should apply to.

  It it set in TerminationHints.checkVars, which is the place where we also check that the user does not bind more extra parameters than present in the predefinition.

instance Lean.Elab.WF.instInhabitedTerminationHints : Inhabited Lean.Elab.WF.TerminationHints

Equations

• Lean.Elab.WF.instInhabitedTerminationHints = { default := { ref := default, termination_by? := default, decreasing_by? := default, extraParams := default } }

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

Equations

• Lean.Elab.WF.TerminationHints.none = { ref := Lean.Syntax.missing, termination_by? := none, decreasing_by? := none, extraParams := 0 }

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

Logs warnings when the TerminationHints are present.

Equations

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

def Lean.Elab.WF.TerminationHints.checkVars (headerParams : Nat) (hints : Lean.Elab.WF.TerminationHints) (value : Lean.Expr) : Lean.MetaM Lean.Elab.WF.TerminationHints

Checks that termination_by binds at most as many variables are present in the outermost lambda of value, and logs (without failing) appropriate errors.

Also remembers extraParams for later use.

Equations

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

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

Takes apart a Termination.suffix syntax object

Equations

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