Support for decreasing_by and termination_by' notations

structure Lean.Elab.WF.TerminationHintValue : Type

• ref : Lean.Syntax
• value : Lean.Syntax

instance Lean.Elab.WF.instInhabitedTerminationHintValue : Inhabited Lean.Elab.WF.TerminationHintValue

Equations

• Lean.Elab.WF.instInhabitedTerminationHintValue = { default := { ref := default, value := default } }

inductive Lean.Elab.WF.TerminationHint : Type

• none: Lean.Elab.WF.TerminationHint
• one: Lean.Elab.WF.TerminationHintValue → Lean.Elab.WF.TerminationHint
• many: Lake.NameMap Lean.Elab.WF.TerminationHintValue → Lean.Elab.WF.TerminationHint

instance Lean.Elab.WF.instInhabitedTerminationHint : Inhabited Lean.Elab.WF.TerminationHint

Equations

• Lean.Elab.WF.instInhabitedTerminationHint = { default := Lean.Elab.WF.TerminationHint.none }

def Lean.Elab.WF.expandTerminationHint (terminationHint? : Option Lean.Syntax) (cliques : Array (Array Lake.Name)) : Lean.MacroM Lean.Elab.WF.TerminationHint

Equations

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

def Lean.Elab.WF.TerminationHint.markAsUsed (t : Lean.Elab.WF.TerminationHint) (clique : Array Lake.Name) : Lean.Elab.WF.TerminationHint

Equations

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

def Lean.Elab.WF.TerminationHint.find? (t : Lean.Elab.WF.TerminationHint) (clique : Array Lake.Name) : Option Lean.Elab.WF.TerminationHintValue

Equations

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

def Lean.Elab.WF.TerminationHint.ensureAllUsed (t : Lean.Elab.WF.TerminationHint) : Lean.MacroM Unit

Equations

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

Support for termination_by notation

structure Lean.Elab.WF.TerminationByElement : Type

• ref : Lean.Syntax
• declName : Lake.Name
• vars : Array Lean.Syntax
• body : Lean.Syntax
• implicit : Bool

instance Lean.Elab.WF.instInhabitedTerminationByElement : Inhabited Lean.Elab.WF.TerminationByElement

Equations

• Lean.Elab.WF.instInhabitedTerminationByElement = { default := { ref := default, declName := default, vars := default, body := default, implicit := default } }

structure Lean.Elab.WF.TerminationByClique : Type

• elements : Array Lean.Elab.WF.TerminationByElement
• used : Bool

inductive Lean.Elab.WF.TerminationBy : Type

• core: Lean.Elab.WF.TerminationHint → Lean.Elab.WF.TerminationBy
• ext: Array Lean.Elab.WF.TerminationByClique → Lean.Elab.WF.TerminationBy

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

Equations

• Lean.Elab.WF.instInhabitedTerminationBy = { default := Lean.Elab.WF.TerminationBy.core default }

inductive Lean.Elab.WF.TerminationWF : Type

• core: Lean.Syntax → Lean.Elab.WF.TerminationWF
• ext: Array Lean.Elab.WF.TerminationByElement → Lean.Elab.WF.TerminationWF

def Lean.Elab.WF.expandTerminationBy (hint? : Option Lean.Syntax) (cliques : Array (Array Lake.Name)) : Lean.MacroM Lean.Elab.WF.TerminationBy

Equations

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

def Lean.Elab.WF.TerminationBy.markAsUsed (t : Lean.Elab.WF.TerminationBy) (cliqueNames : Array Lake.Name) : Lean.Elab.WF.TerminationBy

Equations

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

def Lean.Elab.WF.TerminationBy.find? (t : Lean.Elab.WF.TerminationBy) (cliqueNames : Array Lake.Name) : Option Lean.Elab.WF.TerminationWF

Equations

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

def Lean.Elab.WF.TerminationByClique.allImplicit (c : Lean.Elab.WF.TerminationByClique) : Bool

Equations

• Lean.Elab.WF.TerminationByClique.allImplicit c = Array.all c.elements (fun elem => elem.implicit) 0 (Array.size c.elements)

def Lean.Elab.WF.TerminationByClique.getExplicitElement? (c : Lean.Elab.WF.TerminationByClique) : Option Lean.Elab.WF.TerminationByElement

Equations

• Lean.Elab.WF.TerminationByClique.getExplicitElement? c = Array.find? c.elements fun x => !x.implicit

def Lean.Elab.WF.TerminationBy.ensureAllUsed (t : Lean.Elab.WF.TerminationBy) : Lean.MacroM Unit

Equations

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