From 97f84ccace4e634b4e02178a702818e69292dc9f Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Mon, 8 Jul 2024 22:01:42 +0200
Subject: implement top-level definitions

---
 README.md | 22 ++++++++++++++--------
 1 file changed, 14 insertions(+), 8 deletions(-)

(limited to 'README.md')

diff --git a/README.md b/README.md
index 80cc8ba..4fa6bc7 100644
--- a/README.md
+++ b/README.md
@@ -13,24 +13,30 @@ it probably has lots of bugs as well.
 
 ## example
 
+the file `test/bool.toytt` defines some elementary functions on booleans.
+
 ```
-$ dune exec toytt
-(\b -> bool-elim b at x -> bool [ true => false, false => true ] :: (b : bool) -> bool) false
+toytt> not false
+true : bool
+toytt> and false
+\y -> false : bool -> bool
+toytt> xor true false
 true : bool
+toytt> or true bool
+ ￫ error[E302]
+ 1 | or true bool
+   ^ type mismatch:
+     expected: bool
+        found: type
 ```
 
-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)
 
 - [x] figure out how to recover variable names in pretty-printing so we don't
   have to print de bruijn indices all the time
 - [x] build a better repl
 - [x] improve error messages
-- [ ] implement top-level definitions
+- [x] implement top-level definitions
 - [x] 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
-- 
cgit 1.4.1