structure Lean.Elab.TerminationHints : Type

• terminationBy? : Option Lean.Syntax
• decreasingBy? : Option Lean.Syntax

instance Lean.Elab.instInhabitedTerminationHints : Inhabited Lean.Elab.TerminationHints

Equations

• Lean.Elab.instInhabitedTerminationHints = { default := { terminationBy? := default, decreasingBy? := default } }

def Lean.Elab.addPreDefinitions (preDefs : Array Lean.Elab.PreDefinition) (hints : Lean.Elab.TerminationHints) : Lean.Elab.TermElabM Unit

Equations

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