pairs now associate to the right

diff --git a/Exp.cf b/Exp.cf
index 074fc1509d40f8234a93cfed47d66a52760573a1..9204e56ca919d68d5a88ca62cd870a4084edbce8 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -39,8 +39,9 @@ Comp.       Exp3 ::= "comp" ;
 Glue.       Exp3 ::= "glue" ;
 GlueElem.   Exp3 ::= "glueElem" ;
 System.     Exp3 ::= "[" [Side] "]" ;
-Pair.       Exp3 ::= "(" Exp "," Exp ")" ;
+Pair.       Exp3 ::= "(" Exp "," [Exp] ")" ;
 coercions Exp 3 ;
+separator nonempty Exp "," ;
 
 Dir0.       Dir ::= "0" ;
 Dir1.       Dir ::= "1" ;

diff --git a/Resolver.hs b/Resolver.hs
index a656f1d32930fbf2988092d56dacd533977f81f3..091eeddc070dca22220803aee134f7aab26b0668 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -204,7 +204,10 @@ resolveExp e = case e of
     lams tele (resolveExp t)
   Fst t         -> CTT.Fst <$> resolveExp t
   Snd t         -> CTT.Snd <$> resolveExp t
-  Pair t0 t1    -> CTT.Pair <$> resolveExp t0 <*> resolveExp t1
+  Pair t0 ts    -> do
+    e  <- resolveExp t0
+    es <- mapM resolveExp ts
+    return $ foldr1 CTT.Pair (e:es)
   Let decls e   -> do
     (rdecls,names) <- resolveDecls decls
     CTT.mkWheres rdecls <$> local (insertIdents names) (resolveExp e)

diff --git a/examples/bool.ctt b/examples/bool.ctt
index 8e245107eb3b53c3ef73633d54547baceeee37a9..c796767eee08cb0aa950315513517d3c9f299a9b 100644 (file)
--- a/examples/bool.ctt
+++ b/examples/bool.ctt
@@ -13,7 +13,7 @@ negK : (b : bool) -> Id bool (neg (neg b)) b = split
   false -> refl bool false
 
 negEq : Id U bool bool =
-  <i> glue bool [ (i = 0) -> (bool,(neg,(neg,(negK,negK)))) ]
+  <i> glue bool [ (i = 0) -> (bool,neg,neg,negK,negK) ]
 
 test : bool = transport negEq true
 
@@ -37,7 +37,7 @@ boolToF2K : (b : bool) -> Id bool (f2ToBool (boolToF2 b)) b = split
 
 boolEqF2 : Id U bool F2 =
  -- <i> glue F2 [ (i = 0) -> (bool,(boolToF2,(f2ToBool,(f2ToBoolK,boolToF2K))))]
-  isoId bool F2 boolToF2 f2ToBool f2ToBoolK boolToF2K
+ isoId bool F2 boolToF2 f2ToBool f2ToBoolK boolToF2K
   
 negF2 : F2 -> F2 = subst U (\(X : U) -> (X -> X)) bool F2 boolEqF2 neg
 

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index cb0f4b6a1dccde652c36e28b0d5262bb5d8b1adb..3a76ac92adc27c30a854c6784ffebe1ad3e99c00 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -36,4 +36,4 @@ inv (A : U) (a b : A) (p : Id A a b) : Id A b a = <i> p @ -i
 isoId (A B : U) (f : A -> B) (g : B -> A)
       (s : (y:B) -> Id B (f (g y)) y)
       (t : (x:A) -> Id A (g (f x)) x) : Id U A B =
-      <i> glue B [ (i = 0) -> (A,(f,(g,(s,t)))) ]
+      <i> glue B [ (i = 0) -> (A,f,g,s,t) ]