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 : Lean.Options) :
Bool

Gets the value of the linter.unnecessarySimpa option.

Instances For
    source
    instance Lean.Elab.Tactic.Simpa.instReprUseImplicitLambdaResult :
    Repr Lean.Elab.Term.UseImplicitLambdaResult
    source
    def Lean.Elab.Tactic.Simpa.evalSimpa :
    Lean.Elab.Tactic.Tactic
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For