Zulip Chat Archive
Stream: new members
Topic: How do I ask a tactic to only work on one side
YH (Dec 13 2019 at 23:48):
of an equation or inequality?
Reid Barton (Dec 13 2019 at 23:49):
See https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md#conv
YH (Dec 13 2019 at 23:56):
Can this be used with at? Tried conv_rhs {norm_num} at hm doesn't seem to work.
Alex J. Best (Dec 13 2019 at 23:59):
The syntax is conv_lhs at hm {norm_num} ,
Reid Barton (Dec 13 2019 at 23:59):
Mouse over or whatever you do to see the docstring of the tactic.
Reid Barton (Dec 13 2019 at 23:59):
Or not even the docstring, but the syntax
Kevin Buzzard (Dec 14 2019 at 07:27):
For conv there is a very helpful extended doc in extras with lots of examples. If there are any other issues which you feel would benefit from such an extended doc, I'd be interested to know (take a look at the extras directory to see a few others).
Last updated: Dec 20 2023 at 11:08 UTC