| action | vscode |
|---|---|
| Reload and typecheck | C-c C-l |
| Restart Agda | C-c C-r |
| Compute expression | C-c C-n |
| action | vscode |
|---|---|
Auto (agsy) |
C-c C-a |
| Ask for goal, and context | C-c C-, |
| Ask for goal, context, and expression in hole | C-c C-. |
| Try to use given expr to fill hole ("give") | C-c C-SPC |
| Introduce arguments | C-c C-c |
| Case split (asks for input or names in the hole) | C-c C-c |
| Introduce copattern (don't enter a name) | C-c C-c |
| Attempt to introduce "constructor"* ("refine") | C-c C-r |
| Try to use function in hole, adding holes for args | C-c C-r |
For Emacs, the official documentation is plenty good.
For vim with Cornelis, there are no official bindings, but there are some recommendations in its README.
- 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 kind of a constructor if you squint or if you want to be technical, 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
This is the official, first, and likely most supported editor integration
This is probably the easiest integration to use.
Note that you might need the latest Agda for this.
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.