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.

General function implementing adaptation notes.

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

    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.
    Instances For

      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.
      Instances For

        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.
        Instances For

          Elaborator for adaptation notes.

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