Skip to main content
Join the official 2019 Python Developers SurveyStart the survey!

A rudimentary Jupyter kernel for Agda

Project description

Binder Build Status codecov.io Jupyter Notebook Agda agda-stdlib

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 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 Π
[=

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Files for agda-kernel, version 0.62
Filename, size File type Python version Upload date Hashes
Filename, size agda_kernel-0.62-py3-none-any.whl (20.8 kB) File type Wheel Python version py3 Upload date Hashes View hashes
Filename, size agda_kernel-0.62.tar.gz (15.5 kB) File type Source Python version None Upload date Hashes View hashes

Supported by

Elastic Elastic Search Pingdom Pingdom Monitoring Google Google BigQuery Sentry Sentry Error logging AWS AWS Cloud computing DataDog DataDog Monitoring Fastly Fastly CDN SignalFx SignalFx Supporter DigiCert DigiCert EV certificate StatusPage StatusPage Status page