Zulip Chat Archive

Stream: general

Topic: VScode calc


Patrick Massot (Feb 21 2020 at 12:15):

I have a new idea for our VScode extension experts. Say my goal is A = B. I'd like a key combination which inserts

calc
A = sorry : sorry
... = B : sorry,

The key combination would first insert in the proof script start_calc, where start_calc is a tactic that generate the above string (this is trivial to write) and then would do the analogue of clicking "Try this" to replace start_calc by its output.

Patrick Massot (Feb 21 2020 at 12:15):

And then same with inequalities of course.

Johan Commelin (Feb 21 2020 at 12:22):

Do you want sorry or _?

Johan Commelin (Feb 21 2020 at 12:22):

I would guess that in term mode _ would be more useful.

Patrick Massot (Feb 21 2020 at 12:23):

_ is quicker to erase but it rises an error.

Johan Commelin (Feb 21 2020 at 12:30):

True

Johan Commelin (Feb 21 2020 at 12:30):

That's what you get with error-driven-development (aka term mode)

Anne Baanen (Feb 21 2020 at 12:32):

This seems like a good use case for a hole command!

Patrick Massot (Feb 21 2020 at 12:44):

It can be a hole command, but it would be nice to have a single short-cut that write {!!}, does the Ctrl-shift-. and chooses from the menu. Typing all this is pretty slow (at least on a French keyboard where curly braces are Alt-Gr 4).


Last updated: Dec 20 2023 at 11:08 UTC