A rudimentary Jupyter kernel for Agda
Project description
agda-kernel
An experimental Agda kernel for Jupyter. Used at Nextjournal [nextjournal kernel].
Examples
You can launch the following examples directly via the mybinder interface:
Alternatively, if you have binder, then you can use repo2docker locally:
repo2docker https://github.com/lclem/agda-kernel
Installation
pip install agda_kernel
python -m agda_kernel.install
Syntax highlighting
Syntax highlighting is done separately by Codemirror,
but unfortunately there is no Agda mode packaged with it.
A rudimentary Agda mode for Codemirror can be found in codemirror-agda/agda.js
.
In order to install it, type
make codemirror-install
Agda extension
In order to improve the Jupyter interface,
it is strongly recommended to also install agda-extension
.
Functionality
Each code cell must contain a line of the form module A.B.C where
.
For instance:
module A.B.C where
id : {A : Set} → A → A
id x = x
Upon execution, the file A/B/C.agda
is created containing the cell's contents,
and it is fed to the Agda interpreter (via agda --interaction
).
The results of typechecking the cell are then displayed.
After a cell has been evaluated, one can
-
Run Agsy (auto) by putting the cursor next to a goal
?
and hitting TAB. The hole?
is replaced by the result returned by Agsy, if any, or by{! !}
if no result was found. If there is more than one result, the first ten of them are presented for the user to choose from. -
Refine the current goal by putting the cursor next to a goal
{! !}
and hitting TAB. An optional variable can be provided for case-splitting{! m !}
. -
Show information about the current context, goal, etc.: putting the cursor near a goal/literal and hit SHIFT-TAB.
Editing
Inputting common UNICODE characters is facilitated by the code-completion feature of Jupyter.
- When the cursor is immediately to the right of one of the
base form
symbols hitting TAB will replace it by the correspondingalternate form
. Hitting TAB again will go back to the base form.
base form | alternate form |
---|---|
-> | → |
\ | λ |
< | ⟨ |
B | 𝔹 |
> | ⟩ |
= | ≡ |
top | ⊤ |
/= | ≢ |
bot | ⊥ |
alpha | α |
/\ | ∧ |
e | ε |
/ | ∨ |
emptyset | ∅ |
neg | ¬ |
qed | ∎ |
forall | ∀ |
Sigma | Σ |
exists | ∃ |
Pi | Π |
[= | ⊑ |
Project details
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Hashes for agda_kernel-0.64-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 4087057c311292a3c8ce446acd4db64032c7c1cf0d733e4db0d8b28c497faf8b |
|
MD5 | 7ef10798358b2a648b9f37618a7cd4b5 |
|
BLAKE2b-256 | c40e6c193ad49ff9c3797de2dc1cf31b17495e1b91125e2781bfb942858170a7 |