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 attribute #

source

structure SorryfulInfo :

Type

The information for stored for a decleration 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.

Instances For

source

opaque sorryfulExtension :

Lean.SimplePersistentEnvExtension SorryfulInfo (Array SorryfulInfo)

An enviroment extension containing the information of declerations which carry the sorryful attribute.

source

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.

Instances For

source

def Sorryful_attr :

Lean.ParserDescr

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

Equations