Physlib.Meta.Informal.Basic
Informal definitions and lemmas
This file contains the necessary structures that must be imported into a file for it to contain informal definitions and lemmas.
Everything else about informal definitions and lemmas are in the `Informal.Post` module.
Syntax
Using macros for syntax rewriting works better with the language server compared to `Lake.DSL.LeanLibDecl`. Hovering over any definition of `informal_definition` or `informal_lemma` gives a proper type hint like any proper definition using `def` whereas definitions of `lake_lib` and `lake_exe` don't show docstrings and infer the type `Lean.Name`.
2 declarations
Declaration syntax for informal definitions
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.
Declaration of an informal lemma
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.