Physlib.Meta.Informal.Post

The function evaluates a `ConstantInfo` object $c$ from the Lean environment. It returns `true` if $c$ is a definition whose type is either `InformalDefinition` or `InformalLemma`, and returns `false` otherwise.

Given a Lean declaration metadata object $c$ (of type `ConstantInfo`), this function returns `true` if $c$ is a definition and its type is `InformalLemma`, and returns `false` otherwise.

Given a `ConstantInfo` object $c$, the function returns `true` if $c$ represents an informal definition (specifically, if it is a definition whose type is `InformalDefinition`), and `false` otherwise.

Given a Lean declaration metadata object $c$ of type `ConstantInfo`, this function evaluates the constant to retrieve its corresponding `InformalLemma` structure. The operation is performed within the `CoreM` monad. It expects $c$ to be a definition; if $c$ does not represent a definition, the function will trigger a runtime error.

Given a `ConstantInfo` object $c$ that represents a declaration in the environment, this function retrieves and returns the corresponding `InformalDefinition` structure. The function assumes that $c$ is a definition of type `InformalDefinition`; if $c$ does not correspond to an informal definition, the process will terminate with an error.

Given a Lean declaration metadata object $c$ of type `ConstantInfo`, this function retrieves the string-based identifier (tag) associated with it, provided that $c$ represents either an informal lemma or an informal definition. The function first checks if $c$ is an informal lemma; if so, it extracts its tag. If not, it checks if $c$ is an informal definition and extracts its tag. If $c$ is neither, the function terminates with an error. The operation is executed within the `CoreM` monad and returns a `String`.

The function `Physlib.noInformalLemmas` calculates the total number of informal lemmas present in the $\texttt{Physlib}$ library. Operating within the $\text{CoreM}$ monad, it retrieves all modules imported by $\texttt{Physlib}$, extracts the user-defined constants from each module, and counts those that satisfy the `Informal.isInformalLemma` predicate. The result is returned as a natural number $n \in \mathbb{N}$.

The function `Physlib.noInformalDefs` calculates the total number of informal definitions present in the $\texttt{Physlib}$ library. Operating within the $\text{CoreM}$ monad, it retrieves all modules imported by $\texttt{Physlib}$, extracts the user-defined constants from each module, and counts those that satisfy the `Informal.isInformalDef` predicate. The result is returned as a natural number $n \in \mathbb{N}$.

The function `Physlib.AllInformal` retrieves an array of `ConstantInfo` objects representing all informal results within the $\texttt{Physlib}$ library. Operating within the $\text{CoreM}$ monad, it identifies all modules imported by $\texttt{Physlib}$, extracts the user-defined constants from these modules, and filters the resulting list to include only those constants categorized as an `InformalDefinition` or `InformalLemma` according to the `isInformal` predicate.