/idr-logical-foundations

Logical Foundations in Idris

Primary LanguageIdrisOtherNOASSERTION

Logical Foundations in Idris

Creative Commons License

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