aboutsummaryrefslogtreecommitdiff
path: root/README.md
diff options
context:
space:
mode:
authorDan Rostovtsev <dan@rostovtsev.org>2026-03-29 15:42:46 -0400
committerDan Rostovtsev <dan@rostovtsev.org>2026-03-29 15:42:46 -0400
commit260fd7480c613205ab779b69e354ecf8f8b9a131 (patch)
tree1a9ff75f59bd32d392f5a6ea6036901e24a0ea54 /README.md
parentfb9d9ed9995c6e411f1223d5b53f7b8b6880573e (diff)
Added build instructions to README.
Diffstat (limited to 'README.md')
-rw-r--r--README.md13
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,