Documentation

Lean.Elab.PreDefinition.Main

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

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.

Elaborates the TerminationHint in the clique to TerminationArguments

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