Termination Check!

KonjacSource · Oct 8, 2024 · 3da6a04 · 3da6a04
1 parent 9415ca0
commit 3da6a04
Show file tree

Hide file tree

Showing 12 changed files with 1 addition and 4 deletions.
diff --git a/Draft.shitt → Examples/Draft.shitt b/Draft.shitt → 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 → Examples/Example.shitt b/Example.shitt → Examples/Example.shitt
diff --git a/Example2.shitt → Examples/Example2.shitt b/Example2.shitt → Examples/Example2.shitt
diff --git a/HoTT.shitt → Examples/HoTT.shitt b/HoTT.shitt → Examples/HoTT.shitt
diff --git a/LoadTest.shitt → Examples/LoadTest.shitt b/LoadTest.shitt → Examples/LoadTest.shitt
diff --git a/LoadTest1.shitt → Examples/LoadTest1.shitt b/LoadTest1.shitt → Examples/LoadTest1.shitt
diff --git a/TermTest.shitt → Examples/TermTest.shitt b/TermTest.shitt → Examples/TermTest.shitt
diff --git a/Test1.shitt → Examples/Test1.shitt b/Test1.shitt → Examples/Test1.shitt
diff --git a/Test2.shitt → Examples/Test2.shitt b/Test2.shitt → Examples/Test2.shitt
diff --git a/Test3.shitt → Examples/Test3.shitt b/Test3.shitt → Examples/Test3.shitt
diff --git a/WithoutKTest.shitt → Examples/WithoutKTest.shitt b/WithoutKTest.shitt → Examples/WithoutKTest.shitt
diff --git a/TODO.list b/TODO.list