structure Lean.Elab.TerminationHints : Type

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

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

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