For people who don't wanna use Emacs for whatever reasons.
Feel free to open issues!!!!
- Atom Packages: language-agda
- Binaries: agda
- Ensure you have the Atom package language-agda installed and enabled.
- Ensure you have agda properly installed. Try
agda
in your console. - Install the package:
- from the editor:
Atom > Preferences... > Install
, search foragda-mode
and install - or from a shell:
apm install agda-mode
- If you have Agda installed properly (i.e.
agda
is in the PATH, check it in your console), then it's good to go.
This is an 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-h |
toggle display of implicit arguments | ✓ | |
C-c C-s |
solve constraints | ✓ | |
C-c C-= |
show constraints | ✓ | |
C-c C-? |
show goals | ✓ | |
C-c C-f |
next goal (forward) | ✓ | |
C-c C-b |
previous goal (back) | ✓ | |
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-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-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.
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 |
Keymap | Command | Reason |
---|---|---|
C-c C-x C-d |
remove goals and highlighting (deactivate) | |
C-c C-x M- |
comment/uncomment the rest of the buffer | nope |
- clone the repo and load it as a development package
- open the repo in the development mode
- install dependencies
apm develop agda-mode
atom -d ~/github/agda-mode
npm install
The project is written in TypeScript so you would probably need these:
npm install -g typescript
apm install atom-typescript