agda的基本jupyter内核
agda-kernel的Python项目详细描述
agda内核
一个用于jupyter的实验agda内核。
安装
pip install agda_kernel
python -m agda_kernel.install
语法突出显示
语法突出显示分别由Codemirror，
但不幸的是，它没有打包的agda模式。
代码镜像的基本agda模式可以在codemirror-agda/agda.js中找到。
要安装它，请键入
make codemirror-install
功能性
每个代码单元格必须包含一行module A.B.C where格式的代码。
例如：
moduleA.B.Cwhereid:{A :Set}→ A → A id x = x
执行时，将创建包含单元格内容的文件A/B/C.agda，
它被输入到agda解释器（通过agda --interaction）。
然后显示单元格的类型检查结果。
计算单元后，可以
通过将光标放在目标旁边并点击tab键来运行agsy（auto）。 孔
?被agsy返回的结果（如果有的话）替换， 如果没有结果，也可以通过{! !}。 如果有多个结果，则显示前十个结果供用户选择。通过将光标放在目标
{! !}旁边并点击tab键来优化当前目标。 可以为大小写拆分提供可选变量{! m !}。推断目标/文字的类型，但将光标放在目标/文字附近并按shift-tab键。
示例
您可以直接通过mybinder界面启动以下示例：
编辑
jupyter的代码完成特性有助于输入公共unicode字符。
- 当光标紧靠其中一个
base form符号的右侧时 点击tab将替换为相应的alternate form。 再次按Tab键将返回到基窗体。
| base form | alternate form |
|---|---|
| -> | → |
| \ | λ |
| < | ⟨ |
| B | ? |
| > | ⟩ |
| = | ≡ |
| top | ⊤ |
| /= | ≢ |
| bot | ⊥ |
| alpha | α |
| /\ | ∧ |
| e | ε |
| / | ∨ |
| emptyset | ∅ |
| neg | ¬ |
| qed | ∎ |
| forall | ∀ |
| Sigma | Σ |
| exists | ∃ |
| Pi | Π |
| [= | ⊑ |
欢迎加入QQ群-->： 979659372
