Remove some incidentally commited holes

diff --git a/examples/integer.ctt b/examples/integer.ctt
index 722f6187b5aad9776b5096b8bcf7a322aca5e12a..e3d4d8bcf6c03ed68360edb6664c6aeae36364fa 100644 (file)
--- a/examples/integer.ctt
+++ b/examples/integer.ctt
@@ -45,8 +45,8 @@ fromZK : (a : int) -> Id int (fromZ (toZ a)) a = split
   neg n -> rem n
     where rem : (n : nat) -> Id int (fromZ (toZ (neg n))) (neg n) = split
       zero -> zeroP'
-      suc m -> ? -- refl int (neg (suc n))
-  zeroP @ i -> ? -- <j> zeroP' @ i /\ j
+      suc m -> refl int (neg (suc m))
+  zeroP @ i -> <j> zeroP' @ i /\ j
 
 isoIntZ : Id U Z int = isoId Z int fromZ toZ fromZK toZK