Hot key to pause-unpause the tactic state

Stream: new members

[Robert Culling]

Kia ora koutou :) Is there a keyboard combination for pausing/unpausing the tactic state in VScode?

[Damiano Testa]

You can go to the key bindings of the lean4 extension and define your own combination for Infoview: Toggle Updating. I think that this is not set by default.

[Robert Culling]

Great, thank you. I set a key binding, then the setting dissappeared. So now I can't change the key binding I set. All of a sudden I can't see the option: @ext:leanprover.lean4 Lean 4: Infoview Toggle Update anymore.

Any idea where it went?

[Damiano Testa]

I had a similar experience: I think that when you set it, it disappears from the "extension" key-bindings and it goes in the "user-defined" list. You can find it again if you look for "all" the keybindings.

[Damiano Testa]

I looked at it again: if you remove @ext:leanprover.lean4 from the search filter in the list of key bindings and you instead write lean 4 you should find all the relevant key-bindings, including the ones that you set yourself.

[Robert Culling]

Great, that works. Thank you very much :)