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):

https://github.com/leanprover-community/lean/blob/e611ee5c2bd410148bcd493c58cb17498d667175/src/frontends/lean/tactic_notation.cpp#L271-L274

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):

lean#203


Last updated: Dec 20 2023 at 11:08 UTC