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
Scott Morrison (May 29 2020 at 12:33):
Scott Morrison (May 31 2020 at 01:01):
Last updated: May 12 2021 at 23:13 UTC