Zulip Chat Archive

Stream: general

Topic: interactive calc

Johan Commelin (Apr 28 2020 at 09:02):

Where is the tactic calc defined? I can't find it using grep. I know that the term-mode version is special c++ stuff, but I thought the interactive version was sugar for exact calc, but I can't find this.

Gabriel Ebner (Apr 28 2020 at 09:11):


Johan Commelin (Apr 28 2020 at 09:22):

Ok, thanks! So we can't really change that to refine, right? Because refine isn't yet available at that point.
I am now sometimes writing refine calc .... and I thought it might be nice default behaviour if interactive calc just collected proof obligations in new goals.

Gabriel Ebner (Apr 28 2020 at 09:24):

Of course we can change it to refine. Just replace exact by refine in that line. If refine doesn't exist, it will just fail. :shrug:

Johan Commelin (Apr 28 2020 at 09:26):

Which doesn't seem desirable...

Gabriel Ebner (Apr 28 2020 at 09:28):

refine is defined before exact. I don't think it would cause any issues.

Johan Commelin (Apr 28 2020 at 09:36):


Last updated: Aug 03 2023 at 10:10 UTC