Fix the way @ binds (it is now like normal application)

diff --git a/Exp.cf b/Exp.cf
index 9aff9a04f2424a97582e95b586bbd298c7d6236c..0daa71e07d40aaaf9aef97bd26be63e8f5d9c2ab 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -28,6 +28,7 @@ Path.       Exp  ::= "<" [AIdent] ">" Exp ;
 Fun.        Exp1 ::= Exp2 "->" Exp1 ;
 Pi.         Exp1 ::= [PTele] "->" Exp1 ;
 Sigma.      Exp1 ::= [PTele] "*" Exp1 ;
+AppFormula. Exp2 ::= Exp2 "@" Formula ;
 App.        Exp2 ::= Exp2 Exp3 ;
 IdP.        Exp3 ::= "IdP" Exp4 Exp4 Exp4 ;
 Trans.      Exp3 ::= "transport" Exp4 Exp4 ;
@@ -38,7 +39,6 @@ CompElem.   Exp3 ::= "compElem" Exp4 System Exp4 System ;
 ElimComp.   Exp3 ::= "elimComp" Exp4 System Exp4 ;
 Fst.        Exp4 ::= Exp4 ".1" ;
 Snd.        Exp4 ::= Exp4 ".2" ;
-AppFormula. Exp5 ::= Exp5 "@" Formula ;
 Pair.       Exp5 ::= "(" Exp "," [Exp] ")" ;
 Var.        Exp5 ::= AIdent ;
 PCon.       Exp5 ::= AIdent "{" Exp "}" ; -- c{T A B} x1 x2 @ phi

diff --git a/examples/circle.ctt b/examples/circle.ctt
index 44da52b151cb6a5d9cf3083e45d6844d4b3aa683..3bd19615b9003cdb087aa7b9969cda1ae96d79ac 100644 (file)
--- a/examples/circle.ctt
+++ b/examples/circle.ctt
@@ -33,11 +33,11 @@ loop2'' : loopS1 = compId'' S1 base base loop1 base loop1
 
 mLoop : (x : S1) -> Id S1 x x = split
   base -> loop1
-  loop @ i -> (constSquare S1 base loop1) @ i
+  loop @ i -> constSquare S1 base loop1 @ i
 
 mult (x : S1) : S1 -> S1 = split
   base -> x
-  loop @ i -> (mLoop x) @ i
+  loop @ i -> mLoop x @ i
 
 square (x : S1) : S1 = mult x x
 

diff --git a/examples/higherhit.ctt b/examples/higherhit.ctt
index 4b6b0856506f8276d5e4df3cf2b5ce52119abe1d..4a501a555a5373e465d7247259efed99bbdb7a2c 100644 (file)
--- a/examples/higherhit.ctt
+++ b/examples/higherhit.ctt
@@ -12,7 +12,7 @@ data S1 = base
 
 foo : S1 = base
 
-loop' : Id S1 base base = <i> (loop {S1}) @ i
+loop' : Id S1 base base = <i> loop {S1} @ i
 
 
 -- new
@@ -42,11 +42,9 @@ data setTrunc (A : U)
        , (j=0) -> a
        , (j=1) -> b]
 
--- TODO: fix parsing: no parentheses should be necessary
-
 setTruncSet (A : U) : set (setTrunc A) =
    \(a b : setTrunc A) (p q : Id (setTrunc A) a b) ->
-     <i j> (setTr {setTrunc A} a b p q) @ i @ j
+     <i j> setTr {setTrunc A} a b p q @ i @ j
 
 
 setTruncRec (A : U)

diff --git a/examples/interval.ctt b/examples/interval.ctt
index ca455da5520a4e25d98ac09747946cd960004772..813a881ff34bf86dd57914cb1859f167ab5d593f 100644 (file)
--- a/examples/interval.ctt
+++ b/examples/interval.ctt
@@ -10,4 +10,4 @@ fext (A B : U) (f g : A -> B) (p : (x : A) -> Id B (f x) (g x)) :
   where htpy (x : A) : I -> B = split
           zero    -> f x
           one     -> g x
-          seg @ i -> (p x) @ i
+          seg @ i -> p x @ i

diff --git a/examples/susp.ctt b/examples/susp.ctt
index 1224b1499b8fd0b058a6beee4f2fcf8915ee210c..5d219cec7c7c9d74567b5e575e6db1b20164ae7a 100644 (file)
--- a/examples/susp.ctt
+++ b/examples/susp.ctt
@@ -22,19 +22,19 @@ path : bool -> Id S1 base base = split
 s1ToCircle : sone -> S1 = split\r
   north   -> base\r
   south   -> base\r
-  merid b @ i -> (path b) @ i\r
+  merid b @ i -> path b @ i\r
 \r
-m0 : Id sone north south = <i> (merid{sone} false) @ i\r
+m0 : Id sone north south = <i> merid{sone} false @ i\r
 \r
-m1 : Id sone north south = <i> (merid{sone} true) @ i\r
+m1 : Id sone north south = <i> merid{sone} true @ i\r
 \r
 invm1 : Id sone south north = inv sone north south m1\r
 \r
 circleToS1 : S1 -> sone = split\r
   base -> north\r
-  loop @ i -> (compId sone north south north m0 invm1) @ i\r
+  loop @ i -> compId sone north south north m0 invm1 @ i\r
 \r
-merid1 (b:bool) : Id sone north south = <i>(merid{sone} b)@ i\r
+merid1 (b:bool) : Id sone north south = <i> merid{sone} b @ i\r
 \r
 oc (x:S1) : S1 = s1ToCircle (circleToS1 x)\r
 \r
@@ -52,7 +52,7 @@ lemSquare (A:U) (a b : A) (m0 m1 : Id A a b) :
 coid : (x : sone) -> Id sone (co x) x = split\r
  north -> refl sone north\r
  south -> m1\r
- merid b @ i  -> (ind b) @ i\r
+ merid b @ i  -> ind b @ i\r
   where\r
     F (x:sone) : U = Id sone (co x) x\r
 \r
@@ -69,7 +69,7 @@ s1EqS1 : Id U S1 S1 = compId U S1 sone S1 (inv U sone S1 s1EqCircle) s1EqCircle
 ptU : U = (X : U) * X\r
 \r
 lemPt (A :U) (B:U) (p:Id U A B) (a:A) : Id ptU (A,a) (B,transport p a) =\r
- <i> (p @ i,transport (<j>p @ (i/\j)) a)\r
+ <i> (p @ i,transport (<j> p @ (i/\j)) a)\r
 \r
 Omega (X:ptU) : ptU = (Id X.1 X.2 X.2,refl X.1 X.2)\r
 \r
@@ -87,7 +87,7 @@ s1ToCId (p: Id sone north north) : Id S1 base base
  = <i> transport s1EqCircle (p @ i)\r
 \r
 s1ToCIdInv (p : Id S1 base base) : Id sone north north\r
- = <i> (transport (<j> s1EqCircle @(-j)) (p @ i))\r
+ = <i> (transport (<j> s1EqCircle @ -j) (p @ i))\r
 \r
 loop1S :  Id sone north north = s1ToCIdInv loop1\r
 \r