Underlying structure for notes

This file contains the necessary structures that must be imported into a file for it to be turned into a Lean note.

It allows for the

• note ... command to be used to add notes to a Lean file
• note_attr attribute to be used to display formally verified commands within a note.
• note_attr_informal attribute to be used to display informal commands within a note.

Other results relating to notes are in other files.

structure Physlib.NoteInfo : Type

The information from a note ... command. To be used in a note file

• content : String

  The content of the note.

• fileName : Lean.Name

  The file name where the note came from.

• line : Nat

  The line from where the note came from.

opaque Physlib.noteExtension : Lean.SimplePersistentEnvExtension NoteInfo (Array NoteInfo)

Environment extension to store note ....

def Physlib.note_comment : Lean.ParserDescr

Syntax for the note ... command

Equations

• Physlib.note_comment = Lean.ParserDescr.node `Physlib.note_comment 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "note ") (Lean.ParserDescr.const `str))

def Physlib.elabNote : Lean.Elab.Command.CommandElab

Elaborator for the note ... command

Equations

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

Note attribute

opaque Physlib.noteDeclExtension : Lean.SimplePersistentEnvExtension Lean.Name (Array Lean.Name)

Environment extension to store note_attr.

opaque Physlib.noteAttribute : Unit

The note_attr attribute is used to display formally verified commands within a note.

opaque Physlib.noteInformalDeclExtension : Lean.SimplePersistentEnvExtension Lean.Name (Array Lean.Name)

Environment extension to store note_attr_informal.

opaque Physlib.noteInformalAttribute : Unit

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