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

Equations

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

def Lean.Elab.checkTerminationByHints (preDefs : Array PreDefinition) : 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 should 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 PreDefinition) : TermElabM (Array (Option 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 PreDefinition) : Bool

Equations

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

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

Equations

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

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

Equations

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