From a6ab4f3b2cbcd508d9477930b0a4b860a0bb6e20 Mon Sep 17 00:00:00 2001
From: Joonatan Saarhelo <joon.saar@gmail.com>
Date: Wed, 3 Apr 2019 01:27:31 +0300
Subject: [PATCH] Create README.md

---
 README.md | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 README.md

diff --git a/README.md b/README.md
new file mode 100644
index 0000000..3218f84
--- /dev/null
+++ b/README.md
@@ -0,0 +1,4 @@
+# justified-type-inference
+An implementation of Compositional type inference in Idris with a complete proof
+
+I am now working on a [Coq version of this](https://github.com/joonazan/verified-type-inference) because of a code generation bug in Idris and because typechecking was so slow.