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

def Lean.Elab.instInhabitedTerminationBy.default : TerminationBy

Equations

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

instance Lean.Elab.instInhabitedTerminationBy : Inhabited TerminationBy

Equations

• Lean.Elab.instInhabitedTerminationBy = { default := Lean.Elab.instInhabitedTerminationBy.default }

structure Lean.Elab.DecreasingBy : Type

A single decreasing_by clause

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

def Lean.Elab.instInhabitedDecreasingBy.default : DecreasingBy

Equations

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

instance Lean.Elab.instInhabitedDecreasingBy : Inhabited DecreasingBy

Equations

• Lean.Elab.instInhabitedDecreasingBy = { default := Lean.Elab.instInhabitedDecreasingBy.default }

inductive Lean.Elab.PartialFixpointType : Type

• partialFixpoint : PartialFixpointType
• coinductiveFixpoint : PartialFixpointType
• inductiveFixpoint : PartialFixpointType

def Lean.Elab.instInhabitedPartialFixpointType.default : PartialFixpointType

Equations

• Lean.Elab.instInhabitedPartialFixpointType.default = Lean.Elab.PartialFixpointType.partialFixpoint

instance Lean.Elab.instInhabitedPartialFixpointType : Inhabited PartialFixpointType

Equations

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

structure Lean.Elab.PartialFixpoint : Type

A single partial_fixpoint, inductive_fixpoint or coinductive_fixpoint clause

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

instance Lean.Elab.instInhabitedPartialFixpoint : Inhabited PartialFixpoint

Equations

• Lean.Elab.instInhabitedPartialFixpoint = { default := Lean.Elab.instInhabitedPartialFixpoint.default }

def Lean.Elab.instInhabitedPartialFixpoint.default : 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

• Lean.Elab.instInhabitedTerminationHints = { default := Lean.Elab.instInhabitedTerminationHints.default }

def Lean.Elab.instInhabitedTerminationHints.default : TerminationHints

Equations

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

def Lean.Elab.isInductiveFixpoint : PartialFixpointType → Bool

Equations

• Lean.Elab.isInductiveFixpoint Lean.Elab.PartialFixpointType.inductiveFixpoint = true
• Lean.Elab.isInductiveFixpoint x✝ = false

def Lean.Elab.isCoinductiveFixpoint : PartialFixpointType → Bool

Equations

• Lean.Elab.isCoinductiveFixpoint Lean.Elab.PartialFixpointType.coinductiveFixpoint = true
• Lean.Elab.isCoinductiveFixpoint x✝ = false

def Lean.Elab.isPartialFixpoint : PartialFixpointType → Bool

Equations

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

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

Equations

• Lean.Elab.isLatticeTheoretic p = decide (Lean.Elab.isInductiveFixpoint p = true ∨ Lean.Elab.isCoinductiveFixpoint 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.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.