Zulip Chat Archive

Stream: general

Topic: apply_congr


view this post on Zulip Johan Commelin (May 29 2020 at 12:11):

tactic#apply_congr is really useful, but I think I can't tell it how to name the new hypothesis. Is this because that is a hard problem?

view this post on Zulip Kevin Buzzard (May 29 2020 at 12:13):

Make the user name it?

view this post on Zulip Johan Commelin (May 29 2020 at 12:16):

That's exactly what can't be done atm, I think

view this post on Zulip Kevin Buzzard (May 29 2020 at 12:21):

Oh your question is how a user can control names? In which case I have the same question for interval_cases

view this post on Zulip Scott Morrison (May 29 2020 at 12:33):

issue! :-)

view this post on Zulip Scott Morrison (May 31 2020 at 01:01):

#2881 and #2882


Last updated: May 12 2021 at 23:13 UTC