From 3da6a046e533fd55fbd95e5b7bbd17db3a1e5296 Mon Sep 17 00:00:00 2001
From: KonjacSource <1435771606@qq.com>
Date: Wed, 9 Oct 2024 01:22:23 +0800
Subject: [PATCH] Termination Check!

---
 Draft.shitt => Examples/Draft.shitt               | 2 +-
 Example.shitt => Examples/Example.shitt           | 0
 Example2.shitt => Examples/Example2.shitt         | 0
 HoTT.shitt => Examples/HoTT.shitt                 | 0
 LoadTest.shitt => Examples/LoadTest.shitt         | 0
 LoadTest1.shitt => Examples/LoadTest1.shitt       | 0
 TermTest.shitt => Examples/TermTest.shitt         | 0
 Test1.shitt => Examples/Test1.shitt               | 0
 Test2.shitt => Examples/Test2.shitt               | 0
 Test3.shitt => Examples/Test3.shitt               | 0
 WithoutKTest.shitt => Examples/WithoutKTest.shitt | 0
 TODO.list                                         | 3 ---
 12 files changed, 1 insertion(+), 4 deletions(-)
 rename Draft.shitt => Examples/Draft.shitt (98%)
 rename Example.shitt => Examples/Example.shitt (100%)
 rename Example2.shitt => Examples/Example2.shitt (100%)
 rename HoTT.shitt => Examples/HoTT.shitt (100%)
 rename LoadTest.shitt => Examples/LoadTest.shitt (100%)
 rename LoadTest1.shitt => Examples/LoadTest1.shitt (100%)
 rename TermTest.shitt => Examples/TermTest.shitt (100%)
 rename Test1.shitt => Examples/Test1.shitt (100%)
 rename Test2.shitt => Examples/Test2.shitt (100%)
 rename Test3.shitt => Examples/Test3.shitt (100%)
 rename WithoutKTest.shitt => Examples/WithoutKTest.shitt (100%)
 delete mode 100644 TODO.list

diff --git a/Draft.shitt b/Examples/Draft.shitt
similarity index 98%
rename from Draft.shitt
rename to Examples/Draft.shitt
index 154dea1..492412c 100644
--- a/Draft.shitt
+++ b/Examples/Draft.shitt
@@ -10,7 +10,7 @@ data Vec (A : U) : (_ : N) -> U where
 | nil : ... zero 
 | cons : {n : N} (_ : A) (_ : Vec A n) -> ... (succ n)
 
-axiom fun sorry {A: U} : A
+axiom partial fun sorry {A: U} : A
 
 fun append {A : U} {m n : N} (v : Vec A m) (w : Vec A n) : Vec A (add m n)
 | nil w = w 
diff --git a/Example.shitt b/Examples/Example.shitt
similarity index 100%
rename from Example.shitt
rename to Examples/Example.shitt
diff --git a/Example2.shitt b/Examples/Example2.shitt
similarity index 100%
rename from Example2.shitt
rename to Examples/Example2.shitt
diff --git a/HoTT.shitt b/Examples/HoTT.shitt
similarity index 100%
rename from HoTT.shitt
rename to Examples/HoTT.shitt
diff --git a/LoadTest.shitt b/Examples/LoadTest.shitt
similarity index 100%
rename from LoadTest.shitt
rename to Examples/LoadTest.shitt
diff --git a/LoadTest1.shitt b/Examples/LoadTest1.shitt
similarity index 100%
rename from LoadTest1.shitt
rename to Examples/LoadTest1.shitt
diff --git a/TermTest.shitt b/Examples/TermTest.shitt
similarity index 100%
rename from TermTest.shitt
rename to Examples/TermTest.shitt
diff --git a/Test1.shitt b/Examples/Test1.shitt
similarity index 100%
rename from Test1.shitt
rename to Examples/Test1.shitt
diff --git a/Test2.shitt b/Examples/Test2.shitt
similarity index 100%
rename from Test2.shitt
rename to Examples/Test2.shitt
diff --git a/Test3.shitt b/Examples/Test3.shitt
similarity index 100%
rename from Test3.shitt
rename to Examples/Test3.shitt
diff --git a/WithoutKTest.shitt b/Examples/WithoutKTest.shitt
similarity index 100%
rename from WithoutKTest.shitt
rename to Examples/WithoutKTest.shitt
diff --git a/TODO.list b/TODO.list
deleted file mode 100644
index d41b9c7..0000000
--- a/TODO.list
+++ /dev/null
@@ -1,3 +0,0 @@
-Refactor
-- Mutual recursion.
-- Termination check.
\ No newline at end of file