Documentation

Lean.Elab.PreDefinition.WF.TerminationHint

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: Lean.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 Lean.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 Lean.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 Lean.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.

structure Lean.Elab.WF.TerminationByElement:

Type

ref : Lean.Syntax
declName : Lean.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 Lean.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 Lean.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 Lean.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) :

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 a => !a.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.