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

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 : Syntax
• tactic : TSyntax `Lean.Parser.Tactic.tacticSeq

instance Lean.Elab.instInhabitedDecreasingBy : Inhabited DecreasingBy

Equations

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

inductive Lean.Elab.PartialFixpointType : Type

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

instance Lean.Elab.instInhabitedPartialFixpointType : Inhabited PartialFixpointType

Equations

• Lean.Elab.instInhabitedPartialFixpointType = { default := Lean.Elab.PartialFixpointType.partialFixpoint }

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

Equations

• Lean.Elab.instInhabitedPartialFixpoint = { default := { ref := default, term? := default, fixpointType := default } }

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

Equations

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

def Lean.Elab.isLeast : PartialFixpointType → Bool

Equations

• Lean.Elab.isLeast Lean.Elab.PartialFixpointType.leastFixpoint = true
• Lean.Elab.isLeast x✝ = false

def Lean.Elab.isGreatest : PartialFixpointType → Bool

Equations

• Lean.Elab.isGreatest Lean.Elab.PartialFixpointType.greatestFixpoint = true
• Lean.Elab.isGreatest x✝ = false

def Lean.Elab.isPartial : PartialFixpointType → Bool

Equations

• Lean.Elab.isPartial Lean.Elab.PartialFixpointType.partialFixpoint = true
• Lean.Elab.isPartial x✝ = false

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

Equations

• Lean.Elab.isLatticeTheoretic p = decide (Lean.Elab.isLeast p = true ∨ Lean.Elab.isGreatest p = true)

def Lean.Elab.TerminationHints.none : TerminationHints

Equations

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

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

Logs warnings when the TerminationHints are unexpectedly present.

Equations

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

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

True if any form of termination hint is present.

Equations

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

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

Equations

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

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.

Equations

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

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

Equations

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

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

Equations

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