Physlib.Meta.Linters.Sorry

The `sorryfulExtension` is a persistent environment extension that stores an array of metadata entries, each of type `SorryfulInfo`, corresponding to declarations annotated with the `sorryful` attribute. This extension allows the environment to maintain a registry of declarations that contain the `sorryAx` axiom (commonly known as "sorry"), facilitating the generation of TODO entries and linter checks.

This function, operating within a monad $m$ that has access to the global environment, adds a metadata entry to the `sorryfulExtension`. The entry consists of the declaration's name $declName$, its documentation string $docString$, the source file name $fileName$, and the line number $line$ where the declaration is located.

The `pseudoExtension` is a persistent environment extension used to store and manage information, specifically of type `PseudoInfo`, associated with declarations that have been marked with the `pseudo` attribute.

For a monad $m$ with access to the environment (satisfying `MonadEnv`), the function `addPseudofulEntry` takes a declaration name $\text{declName}$ and modifies the current environment by adding $\text{declName}$ as a new entry to the `pseudoExtension`.

The `sorryful` attribute is a syntax element used to mark Lean declarations. It permits a declaration to contain the `sorryAx` axiom (representing an incomplete proof or definition). Conversely, any declaration marked with the `sorryful` attribute must contain the `sorryAx` axiom.

The `pseudo` attribute is a syntax attribute used to mark Lean declarations. It permits a declaration to contain the `Lean.ofReduceBool` axiom (an axiom used to lift boolean reductions to propositional proofs). Conversely, any declaration marked with the `pseudo` attribute is required to contain the `Lean.ofReduceBool` axiom.