Zulip Chat Archive
Stream: general
Topic: apply_congr
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?
Kevin Buzzard (May 29 2020 at 12:13):
Make the user name it?
Johan Commelin (May 29 2020 at 12:16):
That's exactly what can't be done atm, I think
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
Scott Morrison (May 29 2020 at 12:33):
issue! :-)
Scott Morrison (May 31 2020 at 01:01):
Last updated: Dec 20 2023 at 11:08 UTC