Physlib.Meta.Sorry

The monad $M$ is defined as $M := \text{ReaderT}(\text{Environment}, \text{StateM}(\text{State}))$. It provides a computational context that combines read-only access to the Lean $\text{Environment}$ with a mutable $\text{State}$ for the purpose of traversing and collecting the names of constants that depend on the axioms $\texttt{sorryAx}$ (representing "sorry" proofs) and $\texttt{Lean.ofReduceBool}$ (representing pseudo-definitions).

Given a Lean name $c$ and a set of names representing its ancestors in the dependency graph, $\text{parents}$, the function updates the state within the monad $M$ by determining if the constant $c$ or its dependencies rely on the axioms $\texttt{sorryAx}$ (indicating "sorry" proofs) or $\texttt{Lean.ofReduceBool}$ (indicating pseudo-definitions).

Given an array of Lean names $c$, the function iterates through each name $x \in c$ and applies the $\texttt{collect}$ function with an empty set of ancestor names. This operation updates the internal state of the monad $M$ by identifying whether the constants corresponding to the names in $c$ and their recursive dependencies rely on the axioms $\texttt{sorryAx}$ (representing "sorry" proofs) or $\texttt{Lean.ofReduceBool}$ (representing pseudo-definitions).

Given an array of names $c$, this function identifies all constants in the dependency closure of $c$ that rely on the $\texttt{sorryAx}$ or $\texttt{Lean.ofReduceBool}$ axioms. It returns a pair of arrays $(A, B)$ in the `CoreM` monad, where $A$ contains the names of results depending on $\texttt{sorryAx}$ (representing "sorry" proofs) and $B$ contains the names of results depending on $\texttt{Lean.ofReduceBool}$ (representing pseudo-definitions).

This function, operating within the Lean core environment monad ($\text{CoreM}$), identifies all user-defined constants in the current environment that depend on either the $\texttt{sorryAx}$ or $\texttt{Lean.ofReduceBool}$ axioms. It returns a pair of arrays $(A, B)$, where $A$ is the collection of names of constants whose definitions or proofs rely on the $\texttt{sorryAx}$ axiom (indicating the presence of $\texttt{sorry}$), and $B$ is the collection of names of constants relying on the $\texttt{Lean.ofReduceBool}$ axiom (indicating pseudo-definitions).

The computation retrieves and returns an array containing all names $n$ in the current environment that have been explicitly marked with the `sorryful` attribute.

Within the context of the Lean core environment monad ($\text{CoreM}$), this function retrieves an array of all constant identifiers (names) that have been assigned the `pseudo` attribute.

Within the meta-programming monad ($\text{MetaM}$), this procedure verifies the consistency of the `sorryful` and `pseudo` attributes for all user-defined constants in the environment. Specifically, it checks that a constant is attributed `sorryful` if and only if its definition or proof depends on the `sorryAx` axiom. Simultaneously, it verifies that a constant is attributed `pseudo` if and only if it depends on the `Lean.ofReduceBool` axiom (typically associated with `native_decide`). If any discrepancies are found—either a constant possessing an attribute without the corresponding dependency or a constant having the dependency without the attribute—the function terminates with a detailed error message listing the inconsistent identifiers. Otherwise, it prints a success message indicating that the metadata is correctly applied.