def Lean.Elab.ensureFunIndReservedNamesAvailable (preDefs : Array Lean.Elab.PreDefinition) : Lean.MetaM Unit

Equations

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

def Lean.Elab.checkTerminationByHints (preDefs : Array Lean.Elab.PreDefinition) : Lean.CoreM Unit

Checks consistency of a clique of TerminationHints:

• If not all have a hint, the hints are ignored (log error)
• If one has structural, check that all have it, (else throw error)
• A structural shold not have a decreasing_by (else log error)

Equations

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

def Lean.Elab.elabTerminationByHints (preDefs : Array Lean.Elab.PreDefinition) : Lean.Elab.TermElabM (Array (Option Lean.Elab.TerminationArgument))

Elaborates the TerminationHint in the clique to TerminationArguments

Equations

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

def Lean.Elab.shouldUseStructural (preDefs : Array Lean.Elab.PreDefinition) : Bool

Equations

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

def Lean.Elab.shouldUseWF (preDefs : Array Lean.Elab.PreDefinition) : Bool

Equations

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

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

Equations

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