The "refine" linter

The "refine" linter flags usages of the refine' tactic.

The tactics refine and refine' are similar, but they handle meta-variables slightly differently. This means that they are not completely interchangeable, nor can one completely replace the other. However, refine is more readable and (heuristically) tends to be more efficient on average.

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

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

The refine linter emits a warning on usages of refine'.

partial def Mathlib.Linter.refine.getRefine' : Lean.Syntax → Array Lean.Syntax

getRefine' t returns all usages of the refine' tactic in the input syntax t.

def Mathlib.Linter.refine.getLinterHash (o : Lean.Options) : Bool

The "refine" linter flags usages of the refine' tactic.

The tactics refine and refine' are similar, but they handle meta-variables slightly differently. This means that they are not completely interchangeable, nor can one completely replace the other. However, refine is more readable and (heuristically) tends to be more efficient on average.

Equations

• Mathlib.Linter.refine.getLinterHash o = Lean.Linter.getLinterValue Mathlib.Linter.refine.linter.refine o

def Mathlib.Linter.refine.refineLinter : Lean.Linter

The "refine" linter flags usages of the refine' tactic.

The tactics refine and refine' are similar, but they handle meta-variables slightly differently. This means that they are not completely interchangeable, nor can one completely replace the other. However, refine is more readable and (heuristically) tends to be more efficient on average.

Equations

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