Documentation

Std.Tactic.Simpa

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

The arguments to the simpa family tactics.

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

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

  • simpa [rules, ⋯] using e⋯] 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 ?

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

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

  • simpa [rules, ⋯] using e⋯] 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 ?

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

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

  • simpa [rules, ⋯] using e⋯] 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 ?

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

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

  • simpa [rules, ⋯] using e⋯] 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 ?

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