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.simpaArgsRest : Lean.ParserDescr

The arguments to the simpa family tactics.

def Std.Tactic.Simpa.simpa : Lean.ParserDescr

This is a "finishing" tactic modification of simp. It has two forms.

• simpa [rules, ⋯] using e will simplify the goal and the type of e using rules, then try to close the goal using e.

Simplifying the type of e makes it more likely to match the goal (which has also been simplified). This construction also tends to be more robust under changes to the simp lemma set.

• simpa [rules, ⋯] will simplify the goal and the type of a hypothesis this if present in the context, then try to close the goal using the assumption tactic.

#TODO: implement ?

def Std.Tactic.Simpa.tacticSimpa!_ : Lean.ParserDescr

This is a "finishing" tactic modification of simp. It has two forms.

• simpa [rules, ⋯] using e will simplify the goal and the type of e using rules, then try to close the goal using e.

Simplifying the type of e makes it more likely to match the goal (which has also been simplified). This construction also tends to be more robust under changes to the simp lemma set.

• simpa [rules, ⋯] will simplify the goal and the type of a hypothesis this if present in the context, then try to close the goal using the assumption tactic.

#TODO: implement ?

def Std.Tactic.Simpa.tacticSimpa?_ : Lean.ParserDescr

This is a "finishing" tactic modification of simp. It has two forms.

• simpa [rules, ⋯] using e will simplify the goal and the type of e using rules, then try to close the goal using e.

Simplifying the type of e makes it more likely to match the goal (which has also been simplified). This construction also tends to be more robust under changes to the simp lemma set.

• simpa [rules, ⋯] will simplify the goal and the type of a hypothesis this if present in the context, then try to close the goal using the assumption tactic.

#TODO: implement ?

def Std.Tactic.Simpa.tacticSimpa?!_ : Lean.ParserDescr

This is a "finishing" tactic modification of simp. It has two forms.

• simpa [rules, ⋯] using e will simplify the goal and the type of e using rules, then try to close the goal using e.

Simplifying the type of e makes it more likely to match the goal (which has also been simplified). This construction also tends to be more robust under changes to the simp lemma set.

• simpa [rules, ⋯] will simplify the goal and the type of a hypothesis this if present in the context, then try to close the goal using the assumption tactic.

#TODO: implement ?

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

Gets the value of the linter.unnecessarySimpa option.

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