Physlib.Meta.Informal.SemiFormal

The `wantedExtension` is a persistent environment extension in Lean used to store and manage metadata for "semiformal results." These results are declarations where the signature (the type or the theorem statement) is defined, but the implementation or proof is omitted. The extension stores this information as an array of `WantedInfo` structures, effectively maintaining the "TODO" list of pending proofs and definitions within the environment.

The `semiformal_result` command is a syntax extension used to declare a mathematical definition or a theorem for which the type or proposition is provided, but the actual implementation or proof is omitted. The syntax requires a documentation comment, the keyword `semiformal_result`, a string literal (label), an identifier, and the signature of the declaration. These declarations function as placeholders within the development process—appearing in the library's "TODO" list—and cannot be referenced or utilized by other parts of the formal code.

The function `elabLemmaWanted` is a command elaborator designed to handle the syntax of "semiformal results." When a user declares a statement using the `semiformal_result` command—providing a label, a name, optional arguments, and a result type $T$—this elaborator performs two main tasks. First, it extracts the documentation, the identifier, and source information (such as line number and module) to register them in the `wantedExtension` environment extension for tracking purposes. Second, it generates a noncomputable definition for the identifier with the specified signature by utilizing a temporary axiom as a placeholder. This allows the declaration's type to be recognized by the Lean environment while the actual implementation or proof remains unfinished.