updating names in VSCode

Stream: mathlib4

[Johan Commelin]

I wanted to share a little workflow for updating names (in VSCode). Maybe all you've you know this already. I figured it out yesterday.

1. select i_am_snake_case

2. run the following loop:

   • hit Ctrl-D to select the next occurence
   • if the occurence should be skipped, hit Ctrl-K to "kill" that selection
   • (if necessary, hit Ctrl-U to backtrack)

3. after you have selected all occurences of is_special that need to be changed, make the edit to iAmCamelCase.

[Ruben Van de Velde]

Huh, interesting

[Eric Wieser]

Note that if you put your cursor before i_am_snake_case instead of selecting it, it does a word-based match