Documentation

Lean.Elab.Tactic.Simpa

source
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.

source
def Lean.Elab.Tactic.Simpa.getLinterUnnecessarySimpa (o : Linter.LinterOptions) :
Bool

Gets the value of the linter.unnecessarySimpa option.

Equations
    Instances For
      source
      instance Lean.Elab.Tactic.Simpa.instReprUseImplicitLambdaResult :
      Repr Term.UseImplicitLambdaResult
      Equations
        source
        def Lean.Elab.Tactic.Simpa.evalSimpa :
        Tactic
        Equations
          Instances For