Physlib.Meta.TODO.Basic

The `todoExtension` is a persistent environment extension within the Lean system used to store and manage `TODO` information. It aggregates individual metadata entries of type `todoInfo` into a collection of type `Array todoInfo`.

The syntax for the `TODO` command is defined to accept the keyword `TODO` followed by two string literals. This command is used at the top level (as a command-level syntax) within the Lean environment.

The elaborator `elabTODO` processes the syntax of the command `TODO $t$s`, where $t$ represents a tag and $s$ represents a description string. When invoked, it extracts the content of the tag and the description, determines the current source position (line number) and module name, and creates a `todoInfo` record. This record is then persistently stored in the environment's `todoExtension`. If the syntax is invalid or the position cannot be determined, it raises an error.