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

                  Elaborator for adaptation notes.

                  Equations
                    Instances For