An experimental Agda kernel for Jupyter. Used at Nextjournal [nextjournal kernel].
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
pip install agda_kernel
python -m agda_kernel.install
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
In order to improve the Jupyter interface,
it is strongly recommended to also install agda-extension.
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.
Inputting common UNICODE characters is facilitated by the code-completion feature of Jupyter.
base form symbols
hitting TAB will replace it by the corresponding alternate 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 | Π |
| [= | ⊑ |
FAQs
A rudimentary Jupyter kernel for Agda
We found that agda-kernel demonstrated a healthy version release cadence and project activity because the last version was released less than a year ago. It has 1 open source maintainer collaborating on the project.
Did you know?
Socket for GitHub automatically highlights issues in each pull request and monitors the health of all your open source dependencies. Discover the contents of your packages and block harmful activity before you install or update your dependencies.
Security News
Research
The Socket Research Team breaks down a malicious wrapper package that uses obfuscation to harvest credentials and exfiltrate sensitive data.
Research
Security News
Attackers used a malicious npm package typosquatting a popular ESLint plugin to steal sensitive data, execute commands, and exploit developer systems.
Security News
The Ultralytics' PyPI Package was compromised four times in one weekend through GitHub Actions cache poisoning and failure to rotate previously compromised API tokens.