opaque linter.unnecessarySimpa : Lean.Option Bool

Enables the 'unnecessary simpa' linter. This will report if a use of simpa could be proven using simp or simp at h instead.

def Std.Tactic.Simpa.getLinterUnnecessarySimpa (o : Lean.Options) : Bool

Gets the value of the linter.unnecessarySimpa option.

Equations

• Std.Tactic.Simpa.getLinterUnnecessarySimpa o = Lean.Linter.getLinterValue linter.unnecessarySimpa o

instance Std.Tactic.Simpa.instReprUseImplicitLambdaResult : Repr Lean.Elab.Term.UseImplicitLambdaResult

Equations

• Std.Tactic.Simpa.instReprUseImplicitLambdaResult = { reprPrec := Std.Tactic.Simpa.reprUseImplicitLambdaResult✝ }

def Std.Tactic.Simpa.evalSimpa : Lean.Elab.Tactic.Tactic

Equations

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