The "admit" linter

The "admit" linter flags usages of the admit tactic.

The tactics admit and sorry are synonyms. The use of sorry is much more common and should be preferred.

This linter is an incentive to discourage uses of admit, without being a ban.

opaque Mathlib.Linter.linter.admit : Lean.Option Bool

The admit linter emits a warning on usages of admit.

partial def Mathlib.Linter.AdmitLinter.getAdmit (stx : Lean.Syntax) : Array Lean.Syntax

getAdmit t returns all usages of the admit tactic in the input syntax t.

def Mathlib.Linter.AdmitLinter.admitLinter : Lean.Linter

The "admit" linter flags usages of the admit tactic.

The tactics admit and sorry are synonyms. The use of sorry is much more common and should be preferred.

Equations

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