Support for decreasing_by

structure Lean.Elab.WF.DecreasingByTactic : Type

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

instance Lean.Elab.WF.instInhabitedDecreasingByTactic : Inhabited Lean.Elab.WF.DecreasingByTactic

Equations

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

inductive Lean.Elab.WF.DecreasingBy : Type

• none: Lean.Elab.WF.DecreasingBy
• one: Lean.Elab.WF.DecreasingByTactic → Lean.Elab.WF.DecreasingBy
• many: Lake.NameMap Lean.Elab.WF.DecreasingByTactic → Lean.Elab.WF.DecreasingBy

instance Lean.Elab.WF.instInhabitedDecreasingBy : Inhabited Lean.Elab.WF.DecreasingBy

Equations

• Lean.Elab.WF.instInhabitedDecreasingBy = { default := Lean.Elab.WF.DecreasingBy.none }

def Lean.Elab.WF.expandDecreasingBy? (decreasingBy? : Option Lean.Syntax) (cliques : Array (Array Lake.Name)) : Lean.MacroM Lean.Elab.WF.DecreasingBy

This function takes a user-specified decreasing_by clause (as Sytnax). If it is a decreasingByMany (a set of clauses guarded by the function name) then

• checks that all mentioned names exist in the current declaration
• check that at most one function from each clique is mentioned and sort the entries by function name.

Equations

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

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

Equations

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

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

Equations

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

def Lean.Elab.WF.DecreasingBy.ensureAllUsed (t : Lean.Elab.WF.DecreasingBy) : 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

A single termination_by clause

• ref : Lean.Syntax
• declName : Lake.Name
• vars : Lean.TSyntaxArray [`ident, `Lean.Parser.Term.hole]
• body : Lean.Term
• 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

termination_by clauses, grouped by clique

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

structure Lean.Elab.WF.TerminationBy : Type

A termination_by hint, as specified by the user

• cliques : Array Lean.Elab.WF.TerminationByClique

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

Equations

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

@[inline, reducible]

abbrev Lean.Elab.WF.TerminationWF : Type

A termination_by hint, as applicable to a single clique

Equations

• Lean.Elab.WF.TerminationWF = Array Lean.Elab.WF.TerminationByElement

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

Expands the syntax for a termination_by clause, checking that

• each function is mentioned once
• each function mentioned actually occurs in the current declaration
• if anything is specified, then all functions have a clause
• the else-case (_) occurs only once, and only when needed

NB:

def terminationByElement   := leading_parser ppLine >> (ident <|> hole) >> many (ident <|> hole) >> " => " >> termParser >> optional ";"
def terminationBy          := leading_parser ppLine >> "termination_by " >> many1chIndent terminationByElement

Equations

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

def Lean.Elab.WF.TerminationWF.unexpand (elements : Lean.Elab.WF.TerminationWF) : Lean.MetaM Lean.Syntax

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 : Lean.Elab.WF.TerminationByElement) => 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 : Lean.Elab.WF.TerminationByElement) => !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.