From ef77c527892511ed96db2dee84001f957544dc85 Mon Sep 17 00:00:00 2001 From: William Ball Date: Wed, 28 Aug 2024 11:53:31 -0700 Subject: [PATCH] readme --- README.org | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 README.org diff --git a/README.org b/README.org new file mode 100644 index 0000000..552124b --- /dev/null +++ b/README.org @@ -0,0 +1,5 @@ +* Type Theory and Formal Proofs +This is a partial formalization of the first few chapters of /Type Theory and Formal Proof: An Introduction/ by Nederpelt and Geuvers in Coq. As it stands, the formalization covers up to approximately chapter 3. + +I differ in a few places from their formalization. In particular, I use de Bruijn indices, simply because they are so much more convenient than worrying about \alpha-conversion everywhere. I also include proofs of several exercises from the book. +