Zulip Chat Archive

Stream: new members

Topic: How do I ask a tactic to only work on one side


view this post on Zulip YH (Dec 13 2019 at 23:48):

of an equation or inequality?

view this post on Zulip Reid Barton (Dec 13 2019 at 23:49):

See https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md#conv

view this post on Zulip 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.

view this post on Zulip Alex J. Best (Dec 13 2019 at 23:59):

The syntax is conv_lhs at hm {norm_num} ,

view this post on Zulip Reid Barton (Dec 13 2019 at 23:59):

Mouse over or whatever you do to see the docstring of the tactic.

view this post on Zulip Reid Barton (Dec 13 2019 at 23:59):

Or not even the docstring, but the syntax

view this post on Zulip 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: May 16 2021 at 20:13 UTC