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 Lean.Elab.Tactic.Simpa.getLinterUnnecessarySimpa (o : Linter.LinterOptions) : Bool

Gets the value of the linter.unnecessarySimpa option.

Equations

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

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

Equations

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

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

Equations

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