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

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 partial_fixpoint (throw error)
• If one has structural or partial_fixpoint, check that all have it (else throw error)
• A structural should not have a decreasing_by (else log error)

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

Elaborates the TerminationHint in the clique to TerminationMeasures

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

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

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

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