From: Anders <mortberg@chalmers.se>
Date: Thu, 16 Apr 2015 15:18:59 +0000 (+0200)
Subject: Remove some incidentally commited holes
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=c6ef23cdb88dbcd86891e722d381d520f831bade;p=cubicaltt.git

Remove some incidentally commited holes
---

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