Logical Foundations in Idris

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.

Requirements

• Idris
• Pandoc (Optional)
• Make (Optional)
• Fonts: Montserrat, Fira Sans, and Fira Code (Optional)

Building

Just make and it will typecheck and create a PDF file from the sources in book/.

Solving Exercies

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 testto run the typechecker.

This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License