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

issue! :-)

Scott Morrison (May 31 2020 at 01:01):

#2881 and #2882

Last updated: May 12 2021 at 23:13 UTC