banacorn / Agda Mode
Programming Languages
Labels
Projects that are alternatives of or similar to Agda Mode
agda-mode on Atom
For people who don't wanna use Emacs for whatever reasons.
⚠️ Project status ⏸️
Sorry, people on Atom. Please consider using the new agda-mode on VS Code.
Requirements
- Binaries: agda
Installation
- Install this package:
- from the editor:
Atom > Preferences... > Install, search foragda-modeand install - or from a shell:
apm install agda-mode
- Ensure you have agda properly installed (check this in your console, type
agdaand see if it's in the PATH).
Syntax Highlighting
Unlike on Emacs, agda-mode on Atom doesn't come with syntax highlighting bundled, nor does it highlight your code dynamically on load (yet).
To have your code highlighted:
- Install language-agda:
- from the editor:
Atom > Preferences... > Install, search forlanguage-agdaand install - or from a shell:
apm install language-agda
Extra perk: with language-agda installed, commands such as input-symbol, go-to-definition can be invoked without having to load first.
Recommanded Settings
Enable Scroll Past End
Go to Settings > Editor > Scroll Past End and enable it to allow the editor to
be scrolled past the end of the last line. The reason is that the height of the "panel" at the bottom is constantly changing, and it's pretty annoying to have
the editor jumping up and down with the panel.
Commands
- C-c stands for "press Ctrl and c at the same time"
- When it comes to combos like C-c C-l, you can often slur them into "hold Ctrl while pressing c and then l"
This is an (not so) exhaustive list of available commands:
| Keymap | Command | Global | Goal-specific |
|---|---|---|---|
| C-c C-l | load a file | ✓ | |
| C-c C-x C-q | quit | ✓ | |
| C-c C-x C-r | kill and restart Agda | ✓ | |
| C-c C-x C-c | compile | ✓ | |
| C-c C-x C-a | abort | ✓ | |
| C-c C-x C-h | toggle display of implicit arguments | ✓ | |
| C-c C-= | show constraints | ✓ | |
| C-c C-s | solve constraints | ✓ | |
| C-c C-? | show goals | ✓ | |
| C-c C-f | next goal (forward) | ✓ | |
| C-c C-b | previous goal (back) | ✓ | |
| C-alt-\ or alt-cmd-\ | go to definition | ✓ | |
| C-c C-x C-d | toggle panel docking | ✓ | |
| C-c C-n | compute normal form | ✓ | ✓ |
| C-u C-c C-n | compute normal form (ignoring abstract) | ✓ | ✓ |
| C-u C-u C-c C-n | compute normal form (use show instance) | ✓ | ✓ |
| C-c C-w | why in scope | ✓ | ✓ |
| C-c C-SPC | give | ✓ | |
| C-c C-r | refine | ✓ | |
| C-c C-a | auto | ✓ | |
| C-c C-c | case | ✓ |
Commands listed below support 3 different levels of normalization.
| Keymap | Command | Global | Goal-specific |
|---|---|---|---|
| C-c C-z | search about | ✓ | |
| C-c C-d | infer type | ✓ | ✓ |
| C-c C-o | module contents | ✓ | ✓ |
| C-c C-t | goal type | ✓ | |
| C-c C-e | context | ✓ | |
| C-c C-, | goal type and context | ✓ | |
| C-c C-. | goal type and inferred type | ✓ |
Levels of normalization
| Prefix | Normalization |
|---|---|
| Simplified | |
| C-u | No normalization |
| C-u C-u | Full normalization |
For example, C-u C-c C-d if you want to infer a type without normalizing it.
See Agda:Issue 850 for more discussion.
Unicode input method
To invoke the input method, press \ or alt-/ in .agda or .lagda files.
The key mapping of symbols are the same as in Emacs. For example: \bN for ℕ, \all for ∀, \r or \to for →, etc.
| Keymap | Command |
|---|---|
| \ or alt-/ | input symbol |
| C-u C-x C-= | lookup the key mapping of a symbol |
To customize the keymap, open the settings tab (at the bottom right) and go to Input Method > Keymap extensions
Trouble shooting
Windows 10
If you are having trouble using agda-mode on Windows 10 (symptoms: #97, #98, #110) Please consider follow these instructions and see if it works:
- Go to the system's
Language settings - Select
Administrative language settings - Click
Change system locale... - Check
Beta: Use Unicode UTF-8 for worldwide language support
Contribute
See HACKING