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)
• None have both termination_by and nontermination (throw error)
• If one has structural or partialFixpoint, 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 TerminationMeasure))

Elaborates the TerminationHint in the clique to TerminationMeasures

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.shouldUsepartialFixpoint (preDefs : Array PreDefinition) : Bool

Equations

• Lean.Elab.shouldUsepartialFixpoint preDefs = preDefs.any fun (preDef : Lean.Elab.PreDefinition) => preDef.termination.partialFixpoint?.isSome

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.