From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Fri, 4 Dec 2015 23:05:59 +0000 (-0500)
Subject: minor modification to foo
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=437f259e90e10989464bcee52dac66892f423500;p=cubicaltt.git

minor modification to foo
---

diff --git a/examples/shortsetquot.ctt b/examples/shortsetquot.ctt
index a568240..e52bb55 100644
--- a/examples/shortsetquot.ctt
+++ b/examples/shortsetquot.ctt
@@ -237,19 +237,19 @@ bar (x : bool') : or (Id bool' x true') (Id bool' x false') ->
   inr p -> inr (hinhpr (Id bool' x false') p)
 
 -- finally the map:
-foo (x : bool') : bool = f x rem
+foo (x : bool') (x' : (P' x).1) : bool = f x rem
   where
   rem : or (ishinh (Id bool' x true')).1 (ishinh (Id bool' x false')).1 =
     hinhuniv (or (Id bool' x true') (Id bool' x false'))
              (or (ishinh (Id bool' x true')).1 (ishinh (Id bool' x false')).1,test3 x)
-             (bar x) (K' x)
+             (bar x) x' 
 
 -- > :n testfoo
 -- NORMEVAL: true
 -- Time: 0m0.490s
-testfoo : bool = foo true'
+testfoo : bool = foo true' (K' true')
 
-testfoo' : Id bool (foo true') true = <i> foo true'
+testfoo' : Id bool (foo true' (K' true')) true = <i> foo true' (K' true')