A rudimentary Jupyter kernel for Agda
Project description
agda-kernel
An experimental Agda kernel for Jupyter.
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
Functionality
Each code cell must contain with 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 !}
. -
Infer the type of a goal/literal, but putting the cursor near a goal/literal and hitting SHIFT-TAB.
Examples
You can launch the following examples directly via the mybinder interface:
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.62-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 4315f5db50ceba41aed498f3e54893b3fc7901e26af49511f968e194a0e47581 |
|
MD5 | 8c75746fbb2d08337135d8c0aa24ca1f |
|
BLAKE2b-256 | 3eba225649bc237fb581cb527627fef58d0c70ea3401b03f5ffe864133dfb3b6 |