From 36762e83887b6f917df46c5e40a11d53b697209d Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Tue, 18 Jun 2024 10:53:13 +0200
Subject: add README

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

(limited to 'README.md')

diff --git a/README.md b/README.md
new file mode 100644
index 0000000..9a9f6c9
--- /dev/null
+++ b/README.md
@@ -0,0 +1,40 @@
+# toytt
+
+this is an attempt of mine to implement a typechecker for a minimal dependent
+type theory in the style of martin-löf. at the time of writing this, it has the
+following features:
+
+- type of booleans w/ dependent eliminator
+- pi and sigma connectives
+- universe that contains itself (lol)
+- that's it
+
+it probably has lots of bugs as well.
+
+## example
+
+```
+$ dune exec toytt
+(\b -> bool-elim b at x -> bool [ true => false, false => true ] :: (b : bool) -> bool) false
+true : bool
+```
+
+at the moment the interface is a broken REPL which exits if you make a mistake
+(TODO). the above example illustrates the syntax for lambdas, boolean
+intro & elim, inline type annotations (`::`) and pi types with the boolean
+not-function applied to `false` (which evaluates to `true`).
+
+## todo list (in descending order of importance and/or realizability)
+
+- figure out how to recover variable names in pretty-printing so we don't
+  have to print de bruijn indices all the time
+- implement top-level definitions
+- implement less aggrevating syntax for non-dependent function & pair types
+- add a type of natural numbers
+- replace type-in-type with a proper (cumulative?) hierarchy of universes
+  -> maybe use the mugen library or figure out typical ambiguity?
+- implement inductive types/families
+- implement axioms (probably easy)
+- do HoTT stuff (maybe implement a form of cubical type theory? or stick with
+  book HoTT, which is probably much easier)
+- ...
-- 
cgit 1.4.1