Fix parsing of /\

diff --git a/Exp.cf b/Exp.cf
index 3033a2c0bcc2f99c397adbe7505acb8ff26c785c..398ef387e04f8d0c813a1f1a07cccc51c59e5b1f 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -56,7 +56,7 @@ Side.   Side ::= [Face] "->" Exp ;
 separator Side "," ;
 
 Disj.     Formula  ::= Formula "\\/" Formula1 ;
-Conj.     Formula1 ::= Formula1 "/\\ " Formula2 ; -- Why do we need a space?
+Conj.     Formula1 ::= Formula1 CIdent Formula2 ;
 Neg.      Formula2 ::= "-" Formula2 ;
 Atom.     Formula2 ::= AIdent ;
 Dir.      Formula2 ::= Dir ;
@@ -81,5 +81,7 @@ terminator Tele "" ;
 PTele.    PTele ::= "(" Exp ":" Exp ")" ;
 terminator nonempty PTele "" ;
 
-position token AIdent ((letter|'_')(letter|digit|'\''|'_')*) ;
-separator AIdent "" ;
\ No newline at end of file
+position token AIdent (letter|'_')(letter|digit|'\''|'_')* ;
+separator AIdent "" ;
+
+token CIdent '/''\\' ;
\ No newline at end of file

diff --git a/Resolver.hs b/Resolver.hs
index 40fd0ecf7878ca40502c8f16c30c03167739310e..d2d79aae7203a2c75be8f4235744f39fc7b1911d 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -258,7 +258,7 @@ resolveFormula :: Formula -> Resolver C.Formula
 resolveFormula (Dir d)        = C.Dir <$> resolveDir d
 resolveFormula (Atom i)       = C.Atom <$> resolveName i
 resolveFormula (Neg phi)      = C.negFormula <$> resolveFormula phi
-resolveFormula (Conj phi psi) = C.andFormula <$> resolveFormula phi
+resolveFormula (Conj phi _ psi) = C.andFormula <$> resolveFormula phi
                                 <*> resolveFormula psi
 resolveFormula (Disj phi psi) = C.orFormula <$> resolveFormula phi
                                 <*> resolveFormula psi

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 15663399f37506e9dafbffe92fe3ee136ad3f7ff..da115404ca2ce8c93b9def8903ba0db9bd052008 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -21,7 +21,7 @@ substRefl (A : U) (P : A -> U) (a : A) (e : P a) :
 singl (A : U) (a : A) : U = (x : A) * Id A a x
 
 contrSingl (A : U) (a b : A) (p : Id A a b) :
-  Id (singl A a) (a,refl A a) (b,p) = <i> (p @ i,<j> p @ i /\ j)
+  Id (singl A a) (a,refl A a) (b,p) = <i> (p @ i,<j> p @ i/\j)
 
 J (A : U) (a : A) (C : (x : A) -> Id A a x -> U)
   (d : C a (refl A a)) (x : A) (p : Id A a x) : C x p =