Documentation

Lean.Elab.PreDefinition.Main

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.