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
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: May 17 2021 at 22:15 UTC