VScode calc

Stream: general

[Patrick Massot]

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]

And then same with inequalities of course.

[Johan Commelin]

Do you want sorry or _?

[Johan Commelin]

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

[Patrick Massot]

_ is quicker to erase but it rises an error.

[Johan Commelin]

True

[Johan Commelin]

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

[Anne Baanen]

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

[Patrick Massot]

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