From c6ef23cdb88dbcd86891e722d381d520f831bade Mon Sep 17 00:00:00 2001
From: Anders <mortberg@chalmers.se>
Date: Thu, 16 Apr 2015 17:18:59 +0200
Subject: [PATCH] Remove some incidentally commited holes

---
 examples/integer.ctt | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/examples/integer.ctt b/examples/integer.ctt
index 722f618..e3d4d8b 100644
--- 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
 
-- 
2.34.1