Zulip Chat Archive

Stream: general

Topic: continuity

Johan Commelin (Jul 25 2020 at 20:02):

continuity is great! Thanks @Reid Barton and @Scott Morrison
How hard would it be to have a continuity?

Atm I use show_term {continuity}, but I don't know if that is “best practice”?

Scott Morrison (Jul 26 2020 at 00:00):

I think we should encourage people to use show_term where possible, and only provide ? variations for tactics that can produce something cleverer.

Yury G. Kudryashov (Jul 26 2020 at 00:20):

Is there a vscode shortcut for "replace current tactic with show_term output"?

Yury G. Kudryashov (Jul 26 2020 at 00:21):

If yes, where's the code? I'll try to pretty it to emacs

Bryan Gin-ge Chen (Jul 26 2020 at 00:22):

alt+v will do it

Bryan Gin-ge Chen (Jul 26 2020 at 00:23):

The relevant code is mostly here.

Yury G. Kudryashov (Jul 26 2020 at 00:23):

Thank you.

Patrick Massot (Jul 27 2020 at 10:41):

Could we extend the syntax of continuity to take an optional list of facts? I have a bundled map which has a field asserting some continuity and I'd like the tactic to pick this up.

Patrick Massot (Jul 27 2020 at 15:37):

I also just tried the new continuity tactic (from #3545). I haven't noticed the speedup yet, but I certainly needed the bang version.

Last updated: Dec 20 2023 at 11:08 UTC