Zulip Chat Archive

Stream: general

Topic: Nested congr in conv


view this post on Zulip Floris van Doorn (Jan 05 2021 at 04:51):

Just posted lean#516. Reposting here for some visibility.

In the code snippet below, the second congr raises an error, presumably because I'm already "inside" an earlier congr. In my actual case I wanted to rewrite inside a double integral.

example : ( x y : , x = y) = true :=
begin
  conv { to_lhs, congr, funext, congr, }
end

view this post on Zulip Alex J. Best (Jan 05 2021 at 04:55):

Probably you already know this but just in case a workaround in mathlib is to use nested conv:

example : ( x y : , x = y) = true :=
begin
  conv { to_lhs, congr, funext, conv{ congr, funext,  } }
end

view this post on Zulip Floris van Doorn (Jan 05 2021 at 17:40):

Oh, I did not know that. Thanks!

view this post on Zulip Johan Commelin (Jan 05 2021 at 17:41):

we really need to "fix" conv mode. I think @Eric Wieser already added an exact tactic, but it wouldn't hurt to get some other common goodies.

view this post on Zulip Reid Barton (Jan 05 2021 at 17:43):

I think the issue is more fundamental than goodies

view this post on Zulip Reid Barton (Jan 05 2021 at 17:44):

I'm not sure you can actually navigate to all positions even

view this post on Zulip Eric Wieser (Jan 05 2021 at 17:45):

The exact tactic never made it through PR because I never bothered to add a test

view this post on Zulip Eric Wieser (Jan 05 2021 at 17:45):

I think you _can_ nagivate to all positions using docs#conv.interactive.find

view this post on Zulip Reid Barton (Jan 05 2021 at 17:46):

right, I mean with combinators


Last updated: May 15 2021 at 00:39 UTC