Shortcuts

Samuel Mimram

1 VS Code shortcuts

1.1 OCaml

1.2 Agda

Shortcut Effect
C-c C-l typecheck and highlight the current file
C-c C-, get information about the hole under the cursor
C-c C-. show both the type of the current hole and of the proposed filling
C-c C-space give a solution
C-c C-c case analysis on a variable (≈ an elimination rule)
C-c C-r refine the hole (≈ an introduction rule)
C-c C-a automatic fill

2 Emacs shortcuts

C-x means the “control” and the “x” key at the same time, and M-x means “alt” and “x”. The standard shortcuts are given below.

Shortcut Effect
C-x C-f open/create file
C-x C-s save file
M-w copy
C-w cut
C-y paste
C-s find
tab indent
C-g cancel current operation
C-x o change window under focus
C-x C-c quit emacs

In case you are in a bad state, quit emacs (C-x C-c) and reload the browser tab.

2.1 OCaml

Shortcut Effect
C-c C-e evaluate current function
C-c C-b evaluate the whole file
C-c C-t give the type of the term under the cursor

2.2 Agda

Shortcut Effect
C-c C-l typecheck and highlight the current file
C-c C-, get information about the hole under the cursor
C-c C-. show both the type of the current hole and of the proposed filling
C-c C-space give a solution
C-c C-c case analysis on a variable (≈ an elimination rule)
C-c C-r refine the hole (≈ an introduction rule)
C-c C-a automatic fill