Tactic linters

This file defines passes to run from the tactic analysis framework.

def grindReplacementWith (tacticKind : Lean.SyntaxNodeKind) (reportFailure : Bool := true) (reportSuccess reportSlowdown : Bool := false) (maxSlowdown : Float := 1) : Mathlib.TacticAnalysis.Config

Define a pass that tries replacing a specific tactic with grind.

tacticKind is the SyntaxNodeKind for the tactic's main parser, for example Mathlib.Tactic.linarith.

Equations

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

opaque linter.tacticAnalysis.linarithToGrind : Lean.Option Bool

Debug grind by identifying places where it does not yet supersede linarith.

def linarithToGrind : Mathlib.TacticAnalysis.Config

Debug grind by identifying places where it does not yet supersede linarith.

Equations

• linarithToGrind = grindReplacementWith `Mathlib.Tactic.linarith

opaque linter.tacticAnalysis.omegaToGrind : Lean.Option Bool

Debug grind by identifying places where it does not yet supersede omega.

def omegaToGrind : Mathlib.TacticAnalysis.Config

Debug grind by identifying places where it does not yet supersede omega.

Equations

• omegaToGrind = grindReplacementWith `Lean.Parser.Tactic.omega

opaque linter.tacticAnalysis.ringToGrind : Lean.Option Bool

Debug grind by identifying places where it does not yet supersede ring.

def ringToGrind : Mathlib.TacticAnalysis.Config

Debug grind by identifying places where it does not yet supersede ring.

Equations

• ringToGrind = grindReplacementWith `Mathlib.Tactic.RingNF.ring

opaque linter.tacticAnalysis.rwMerge : Lean.Option Bool

Suggest merging two adjacent rw tactics if that also solves the goal.

def rwMerge : Mathlib.TacticAnalysis.Config

Suggest merging two adjacent rw tactics if that also solves the goal.

Equations

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

opaque linter.tacticAnalysis.mergeWithGrind : Lean.Option Bool

Suggest merging tac; grind into just grind if that also solves the goal.

def mergeWithGrind : Mathlib.TacticAnalysis.Config

Suggest merging tac; grind into just grind if that also solves the goal.

Equations

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

opaque linter.tacticAnalysis.terminalToGrind : Lean.Option Bool

Suggest replacing a sequence of tactics with grind if that also solves the goal.

def terminalToGrind : Mathlib.TacticAnalysis.Config

Suggest replacing a sequence of tactics with grind if that also solves the goal.

Equations

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

opaque linter.tacticAnalysis.introMerge : Lean.Option Bool

Suggest merging two adjacent intro tactics which don't pattern match.

def introMerge : Mathlib.TacticAnalysis.Config

Suggest merging two adjacent intro tactics which don't pattern match.

Equations

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