From 260fd7480c613205ab779b69e354ecf8f8b9a131 Mon Sep 17 00:00:00 2001
From: Dan Rostovtsev <dan@rostovtsev.org>
Date: Sun, 29 Mar 2026 15:42:46 -0400
Subject: Added build instructions to README.

---
 README.md | 13 +++++++++++++
 1 file changed, 13 insertions(+)

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,
-- 
cgit v1.3