Basic underlying structure for TODOs.

structure PhysLean.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 PhysLean.todoExtension : Lean.SimplePersistentEnvExtension todoInfo (Array todoInfo)

Environment extension to store todo ....

def PhysLean.todo_comment : Lean.ParserDescr

Syntax for the TODO ... command.

Equations

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

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

Elaborator for the TODO ... command

Equations

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