HoTT-UF-Agda-Lecture-Notes:关于使用Agda的数学的单价基础的讲义

Agda数学的单价基础简介 新的。 Agda文件的模块化版本位于 ，名称为MGS*.lagda 。 生成讲义的资源可在以下位置获得 需要Agda 。 请查阅以帮助您为Midlands研究生院设置Agda和Emacs。 （literate） *.lagda文件用于使用脚本./build生成html页面。 本作也产生./agda/*.agda使用文件illiterator.hs 。 该方案agdatomd.hs从转换.lagda到.md由脚本使用fastloop 。 该脚本与jekyll serve -watch --incremental一起用于编辑注释，因此更新后仅需要在浏览器中重新加载页面即可查看。 脚本slowloop具有相同的目的，但是通过脚本generatehtml调用了Agda而不是agdatomd ，因此我们在html页面中突出显示了语法。 根据更改的lagda