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.

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

General function implementing adaptation notes.

def adaptationNoteCmd : Lean.ParserDescr

#adaptation_note /-- comment -/ adds an adaptation note to the current file. 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.

This syntax works as a command, or inline in tactic or term mode.

def «tactic#adaptation_note_» : Lean.ParserDescr

#adaptation_note /-- comment -/ adds an adaptation note to the current file. 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.

This syntax works as a command, or inline in tactic or term mode.

def adaptationNoteTermStx : Lean.ParserDescr

#adaptation_note /-- comment -/ adds an adaptation note to the current file. 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.

This syntax works as a command, or inline in tactic or term mode.

def adaptationNoteTermElab : Lean.Elab.Term.TermElab

Elaborator for adaptation notes.