Documentation

Mathlib.Tactic.AdaptationNote

Adaptation notes #

This file defines a #adaptation_note command. Adaptation notes are comments that are used to indicate that a piece of code has been changed to accommodate a change in Lean core. They typically require further action/maintenance to be taken in the future.

source
def reportAdaptationNote (f : Lean.Syntax → Lean.Meta.Tactic.TryThis.Suggestion) :
Lean.MetaM Unit

General function implementing adaptation notes.

Equations
  • One or more equations did not get rendered due to their size.
source
def adaptationNoteCmd :
Lean.ParserDescr

Adaptation notes are comments that are used to indicate that a piece of code has been changed to accommodate a change in Lean core. They typically require further action/maintenance to be taken in the future.

Equations
  • One or more equations did not get rendered due to their size.
source
def «tactic#adaptation_note_» :
Lean.ParserDescr

Adaptation notes are comments that are used to indicate that a piece of code has been changed to accommodate a change in Lean core. They typically require further action/maintenance to be taken in the future.

Equations
  • One or more equations did not get rendered due to their size.
source
def adaptationNoteTermStx :
Lean.ParserDescr

Adaptation notes are comments that are used to indicate that a piece of code has been changed to accommodate a change in Lean core. They typically require further action/maintenance to be taken in the future.

Equations
  • One or more equations did not get rendered due to their size.
source
def adaptationNoteTermElab :
Lean.Elab.Term.TermElab

Elaborator for adaptation notes.

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