From 437f259e90e10989464bcee52dac66892f423500 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Fri, 4 Dec 2015 18:05:59 -0500 Subject: [PATCH] minor modification to foo --- examples/shortsetquot.ctt | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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 = foo true' +testfoo' : Id bool (foo true' (K' true')) true = foo true' (K' true') -- 2.34.1