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: Dec 20 2023 at 11:08 UTC