Tactic linters

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

def Mathlib.TacticAnalysis.terminalReplacement (oldTacticName newTacticName : String) (oldTacticKind : Lean.SyntaxNodeKind) (newTactic : Lean.Syntax → Lean.MVarId → Lean.MetaM (Lean.TSyntax `tactic)) (reportFailure : Bool := true) (reportSuccess reportSlowdown : Bool := false) (maxSlowdown : Float := 1) : Config

Define a pass that tries replacing one terminal tactic with another.

newTacticName is a human-readable name for the tactic, for example "linarith". This can be used to group messages together, so that ring, ring_nf, ring1, ... all produce the same message.

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

newTactic stx goal selects the new tactic to try, which may depend on the old tactic invocation in stx and the current goal.

Equations

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

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

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

tacticName is a human-readable name for the tactic, for example "linarith". This can be used to group messages together, so that ring, ring_nf, ring1, ... all produce the same message.

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.regressions.linarithToGrind : Lean.Option Bool

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

def linarithToGrindRegressions : Mathlib.TacticAnalysis.Config

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

Equations

• linarithToGrindRegressions = Mathlib.TacticAnalysis.grindReplacementWith "linarith" `Mathlib.Tactic.linarith

opaque linter.tacticAnalysis.regressions.ringToGrind : Lean.Option Bool

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

def ringToGrindRegressions : Mathlib.TacticAnalysis.Config

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

Equations

• ringToGrindRegressions = Mathlib.TacticAnalysis.grindReplacementWith "ring" `Mathlib.Tactic.RingNF.ring

opaque linter.tacticAnalysis.regressions.omegaToCutsat : Lean.Option Bool

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

def omegaToCutsatRegressions : Mathlib.TacticAnalysis.Config

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

Equations

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

opaque linter.tacticAnalysis.omegaToCutsat : Lean.Option Bool

Report places where omega can be replaced by cutsat.

def omegaToCutsat : Mathlib.TacticAnalysis.Config

Report places where omega can be replaced by cutsat.

Equations

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

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.