用 Arend 写证明的交互式教程

ITP-Ard 也就是 Interactive Tutorial for Proof in Arend。整个教程由一组 Arend 文件组成， 教学文本被放在了注释之中，而更多的篇幅留给了由具体代码组成的例子与习题。 读者在阅读例子的时候可以利用 IDE 工具辅助理解，遇到习题也可以在 IDE 的辅助下练习， 并由 Arend 验证证明的正确性。如果证明遇到困难，也可以在参考答案中寻求灵感。

食用方法

1. 打开 IntelliJ IDEA（Community 或者 Ultimate 都可以）
2. 在设置中安装插件 Arend
3. （可选）换一个方便阅读注释的主题（这里推荐一下从隔壁 Rider 移植过来的主题）
4. （可选）如果想记录一下自己写的证明可以 Fork 一下本项目
5. 克隆项目至本地并用 IDEA 打开，根据 arend 插件的弹窗提示安装依赖
6. 教程被放在了 src 目录下，以 itp + 编号 + 名称.ard 命名，参考答案文件名以 _ans.ard 结尾