# Support for `termination_by` notation #

source
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

Instances For

source
instance Lean.Elab.instInhabitedTerminationBy :
Inhabited TerminationBy
Equations

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

source
def Lean.Elab.instInhabitedTerminationBy.default :
TerminationBy
Equations

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

Instances For

source
structure Lean.Elab.DecreasingBy :
Type

A single `decreasing_by` clause

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

Instances For

source
def Lean.Elab.instInhabitedDecreasingBy.default :
DecreasingBy
Equations

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

Instances For

source
instance Lean.Elab.instInhabitedDecreasingBy :
Inhabited DecreasingBy
Equations

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

source
inductive Lean.Elab.PartialFixpointType :
Type

- partialFixpoint : PartialFixpointType
- coinductiveFixpoint : PartialFixpointType
- inductiveFixpoint : PartialFixpointType

Instances For

source
instance Lean.Elab.instInhabitedPartialFixpointType :
Inhabited PartialFixpointType
Equations

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

source
def Lean.Elab.instInhabitedPartialFixpointType.default :
PartialFixpointType
Equations

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

Instances For

source
structure Lean.Elab.PartialFixpoint :
Type

A single `partial_fixpoint`, `inductive_fixpoint` or `coinductive_fixpoint` clause

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

Instances For

source
instance Lean.Elab.instInhabitedPartialFixpoint :
Inhabited PartialFixpoint
Equations

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

source
def Lean.Elab.instInhabitedPartialFixpoint.default :
PartialFixpoint
Equations

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

Instances For

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

Instances For

source
def Lean.Elab.instInhabitedTerminationHints.default :
TerminationHints
Equations

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

Instances For

source
instance Lean.Elab.instInhabitedTerminationHints :
Inhabited TerminationHints
Equations

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

source
def Lean.Elab.isInductiveFixpoint :
PartialFixpointType → Bool
Equations

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

Instances For

source
def Lean.Elab.isCoinductiveFixpoint :
PartialFixpointType → Bool
Equations

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

Instances For

source
def Lean.Elab.isPartialFixpoint :
PartialFixpointType → Bool
Equations

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

Instances For

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

- Lean.Elab.isLatticeTheoretic p = decide (Lean.Elab.isInductiveFixpoint p = true ∨ Lean.Elab.isCoinductiveFixpoint p = true)

Instances For

source
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 }

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For