Underlying structure for remarks

structure PhysLean.RemarkInfo : Type

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

• content : String

  The content of the remark.

• fileName : Lean.Name

  The file name where the remark came from.

• line : Nat

  The line from where the remark came from.

• name : Lean.Name

  The name of the remark.

• nameSpace : Lean.Name

  The namespace of the remark.

opaque PhysLean.remarkExtension : Lean.SimplePersistentEnvExtension RemarkInfo (Array RemarkInfo)

Environment extension to store remark ....

def PhysLean.remark_syntax : Lean.ParserDescr

A remark is a string used for important information.

Equations

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

def PhysLean.elabRemark : Lean.Elab.Command.CommandElab

Elaborator for the note ... command

Equations

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