This is a translation of Logical Foundations in Coq by Benjamin C. Pierce et al. It might also use Software Foundations in Idris (2016) as a reference.
- Idris
- Pandoc (Optional)
- Make (Optional)
- Fonts: Montserrat, Fira Sans, and Fira Code (Optional)
Just make
and it will typecheck and create a PDF file from the sources in
book/
.
Important: Per Benjamin C. Pierce request, do not post your solutions in a public medium. (Including GitHub/GitLab/etc)
Just replace the type holes (?type_hole
) for your solutions and run make test
to run the typechecker.
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License