README

clarus · Mar 24, 2015 · 319e74a · 319e74a
1 parent 94abd32
commit 319e74a
Showing 1 changed file with 19 additions and 1 deletion.
diff --git a/README.md b/README.md
@@ -1,2 +1,20 @@
-# False
+# Falso
 A proof of false.
+
+This is an implementation in Coq of the [Falso](http://inutile.club/estatis/falso/) proof system.
+
+## Use
+Install with OPAM for Coq:
+
+    opam repo add coq-stable https://github.com/coq/repo-stable.git
+    opam install coq:falso
+
+In a tedious development:
+
+    Require Import Falso.All.
+
+    Lemma hard : forall (A : Prop), A.
+      destruct falso.
+    Qed.
+
+    Print Assumptions hard.