Basic underlying structure for TODOs.

structure Physlib.todoInfo : Type

The information from a TODO ... command.

• 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.

• tag : String

  The tag of the TODO item

opaque Physlib.todoExtension : Lean.SimplePersistentEnvExtension todoInfo (Array todoInfo)

Environment extension to store todo ....

def Physlib.todo_comment : Lean.ParserDescr

Syntax for the TODO ... command.

Equations

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

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

Elaborator for the TODO ... command

Equations

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