OTT Done

KonjacSource · Nov 9, 2024 · df9896b · df9896b
1 parent a56b42e
commit df9896b
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/Examples/Example.shitt b/Examples/Example.shitt
@@ -19,6 +19,9 @@ fun J {A : U} {a : A} (P : (b : A) -> Id a b -> U) (p : P a (refl _)) (b : A) (e
 fun add (m n : N) : N where  
 | zero n = n
 | (succ m) n = succ (add m n)
+| m (succ n) = succ (add m n)
+
+#eval (\ m n . add m (succ n))
 
 data Vec (A : U) : (_ : N) -> U where 
 | nil : ... zero 

diff --git a/README.md b/README.md
@@ -38,10 +38,10 @@ ghci> run "Eaxmple.shitt"
 - [x] Module system (very naive)
 - [x] Mutual recursion
 - [x] Termination checking
+- [x] [OTT](https://github.com/KonjacSource/ShOTT)
 
 ## TODO
 
-- [ ] OTT
 - [ ] Operators
 - [ ] Universe polymorphism
 - [ ] Positive checking for data types