| action | spacemacs | vscode |
|---|---|---|
| Reload and typecheck | SPC m l | C-c C-l |
| Restart Agda | SPC m x r | C-c C-r |
| Compute expression | SPC m n | C-c C-n |
| action | spacemacs | vscode |
|---|---|---|
Auto (agsy) |
SPC m a | C-c C-a |
| Ask for goal, and context | SPC m , | C-c C-, |
| Ask for goal, context, and expression in hole | SPC m . | C-c C-. |
| Try to use given expr to fill hole ("give") | SPC m SPC | C-c C-SPC |
| Introduce arguments | SPC m c | C-c C-c |
| Case split (asks for input or names in the hole) | SPC m c | C-c C-c |
| Introduce copattern (don't enter a name) | SPC m c | C-c C-c |
| Attempt to introduce "contructor"* ("refine") | SPC m r | C-c C-r |
| Try to use function in hole, adding holes for args | SPC m r | C-c C-r |
- literally a constructor for a type, whose types matches - if ambiguous, the refine won't succeed
- a lambda with as many arguments as possible - this is actually technically a constructor, for the function type (
->) - a record with the required fields for the current type, with holes for the field values
- !VERY USEFUL! - if you have a function name in the hole, if the return type matches the goal, the function will be introduced with holes for its arguments
The instructions for vscode should be almost the same, except you install agda-mode instead
Some git repos for agda courses:
Nice exercises and approach (imo), with the huge bonus of having recorded video lectures.
PLFA - A loose adaptation of the popular Coq based book to Agda.
Good for a gentle introduction, and some exercises. Also for lambda calculus related things in Agda.
You can get a set up emacs agda environment in your browser at this website: https://agdapad.quasicoherent.io/
Additionally, if you send someone the link to the same session, you can work together.