Physlib.Meta.Notes.Basic

The `Physlib.noteExtension` is a persistent environment extension in Lean designed to store and manage information associated with the `note` command. It maintains a state consisting of an array of `NoteInfo` objects, allowing metadata and documentation notes to be preserved across different files and sessions within the Lean environment.

The definition specifies the syntax for the `note` command, which allows a user to provide a string literal $s$ as an annotation within the Lean environment. The command is structured as `note` $s$, where $s$ is a string.

The definition `elabNote` serves as the command elaborator for the `note` syntax. When the command `note s` is invoked, where $s$ is a string literal, the elaborator extracts the text content of $s$, the name of the current module, and the line number of the command's occurrence. This metadata is then bundled into a `NoteInfo` structure and registered within the persistent environment extension `noteExtension` to facilitate the tracking of notes within the Lean environment.

The `Physlib.noteDeclExtension` is a persistent environment extension used to store a collection of names of declarations that have been tagged with the `note_attr` attribute. This extension maintains these names in an array, allowing the Lean environment to track which formal commands are associated with the note-taking system.

The `noteAttribute` is a constant of type unit representing the `note_attr` attribute. This attribute is used to tag and display formally verified commands within a note.

The `Physlib.noteInformalDeclExtension` is a persistent environment extension designed to store and manage declarations associated with the `note_attr_informal` attribute. Specifically, it is a `SimplePersistentEnvExtension` that maps Lean `Name` identifiers to an `Array` of `Name` identifiers, allowing informal commands and notes to be tracked within the Lean environment.

The `note_attr_informal` attribute is a marker used to display informal commands within a Lean note.