Physlib.Meta.Informal.Basic

This command defines a macro `informal_definition` used to declare placeholder definitions within the library. It allows a user to specify a name and a body (value) using the syntax `informal_definition [name] [body]`, which the macro then expands into a standard Lean definition of the type `InformalDefinition`. This mechanism is designed to document mathematical or physical concepts that are intended for future formalization, allowing them to retain docstrings, attributes, and proper language server support.

The `informal_lemma` macro is a syntactic construct used to declare a placeholder for a mathematical lemma that has not yet been formalized. When invoked using the syntax `informal_lemma <name> <body\>`, it defines an object of type `InformalLemma`. This allows a contributor to outline the mathematical or physical content of a lemma and specify relevant references within a docstring before a formal proof is implemented.