1 files changed, 13 insertions, 0 deletions
diff --git a/README.md b/README.md
index 19c9833..60b3e9a 100644
--- a/README.md
+++ b/README.md
@@ -14,6 +14,19 @@ Based off of the untyped weak call-by-value lambda calculus in [1].
 
 - Uniform Confluence
 
+## Building
+
+Requirements:
+
+- [rocq](https://rocq-prover.org/)
+
+The project is built with the GNU build system, but skips the
+configure step. Building is a one-liner.
+
+```
+$ make
+```
+
 ## Citations
 
 1. Forster, Smolka 2017,