The linter for sorry declarations and the sorryful attribute

This module defines an attribute sorryful and a linter noSorry.

The attribute sorryful adds the declaration to an environment extension sorryfulExtension which can be used to create TODO entries.

The linter noSorry checks for declarations that contain the sorryAx axiom if and only if it has the sorryful attribute.

Coloring sorryful

It is possible to color the sorryful attribute in VSCode. This is part of the .vscode/settings.json file, but requires the TODO Highlight extension to be downloaded.

The sorryful environment extension

structure SorryfulInfo : Type

The information for stored for a declaration marked with sorryful.

• name : Lean.Name

  Name of result.

• docstring : String

  The docstring of the result.

• fileName : Lean.Name

  The file name where the note came from.

• line : Nat

  The line from where the note came from.

opaque sorryfulExtension : Lean.SimplePersistentEnvExtension SorryfulInfo (Array SorryfulInfo)

An environment extension containing the information of declarations which carry the sorryful attribute.

def addSorryfulEntry {m : Type → Type} [Lean.MonadEnv m] (declName : Lean.Name) (docString : String) (fileName : Lean.Name) (line : Nat) : m Unit

Adds an entry to sorryfulExtension.

Equations

• One or more equations did not get rendered due to their size.

The psudo environment extension

structure PseudoInfo : Type

The information for stored for a declaration marked with pseudo.

• name : Lean.Name

  Name of result.

opaque pseudoExtension : Lean.SimplePersistentEnvExtension PseudoInfo (Array PseudoInfo)

An environment extension containing the information of declarations which carry the pseudo attribute.

def addPseudofulEntry {m : Type → Type} [Lean.MonadEnv m] (declName : Lean.Name) : m Unit

Adds an entry to pseudoExtension.

Equations

• addPseudofulEntry declName = Lean.modifyEnv fun (x : Lean.Environment) => Lean.PersistentEnvExtension.addEntry pseudoExtension x { name := declName }

The sorryful attribute

def Sorryful_attr : Lean.ParserDescr

The sorryful attribute allows declarations to contain the sorryAx axiom. In converse, a declaration with the sorryful attribute must contain the sorryAx axiom.

Equations

• Sorryful_attr = Lean.ParserDescr.node `Sorryful_attr 1024 (Lean.ParserDescr.nonReservedSymbol "sorryful" false)

The pseudo attribute

def Pseudo_attr : Lean.ParserDescr

The pseudo attribute allows declarations to contain the Lean.ofReduceBool axiom. In converse, a declaration with the pseudo attribute must contain the Lean.ofReduceBool axiom.

Equations

• Pseudo_attr = Lean.ParserDescr.node `Pseudo_attr 1024 (Lean.ParserDescr.nonReservedSymbol "pseudo" false)