diff --git a/ats-format.cabal b/ats-format.cabal
--- a/ats-format.cabal
+++ b/ats-format.cabal
@@ -1,5 +1,5 @@
 name:                ats-format
-version:             0.1.0.11
+version:             0.1.0.12
 synopsis:            A source-code formatter for ATS
 description:         An opinionated source-code formatter for ATS (http://www.ats-lang.org/).
 homepage:            https://hub.darcs.net/vmchale/ats-format#readme
diff --git a/src/Language/ATS/Lexer.x b/src/Language/ATS/Lexer.x
--- a/src/Language/ATS/Lexer.x
+++ b/src/Language/ATS/Lexer.x
@@ -85,7 +85,7 @@
 
 @at_brace = \@ ($white | @block_comment)* \{
 
-@operator = "+" | "-" | "*" | "/" | ".." | "!=" | ">=" | "<=" | "==" | "=" | "~" | "&&" | "||" | ":=" | ".<" | ">." | "<" | ">" | ">>" | "?" | "?!" | "#[" -- TODO context so tilde doesn't follow |
+@operator = "+" | "-" | "*" | "/" | ".." | "!=" | ">=" | "<=" | "==" | "=" | "~" | "%" | "&&" | "||" | ":=" | ".<" | ">." | "<" | ">" | ">>" | "?" | "?!" | "#[" -- TODO context so tilde doesn't follow |
 
 @double_parens = "(" @block_comment ")" | "()"
 @double_braces = "{" @block_comment "}" | "{}"
diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y
--- a/src/Language/ATS/Parser.y
+++ b/src/Language/ATS/Parser.y
@@ -104,6 +104,7 @@
     openParen { Special $$ "(" }
     signature { SignatureTok _ $$ }
     comma { Special $$ "," }
+    percent { Operator $$ "%" }
     geq { Operator $$ ">=" }
     leq { Operator $$ "<=" }
     neq { Operator $$ "!=" }
@@ -358,7 +359,6 @@
               | include {% Left $ Expected $1 "Expression" "include" }
               | staload {% Left $ Expected $1 "Expression" "staload" }
               | overload {% Left $ Expected $1 "Expression" "overload" }
-              | prval {% Left $ Expected $1 "Expression" "prval" }
               | var {% Left $ Expected $1 "Expression" "var" }
               | Termetric {% Left $ Expected (fst $1) "Expression" "termetric" }
               | fromVT {% Left $ Expected $1 "Expression" "?!" }
@@ -381,7 +381,7 @@
             
 -- | Parse a universal quantifier on a type
 Universal : lbrace Args rbrace { Universal $2 Nothing Nothing }
-          | lbrace Args vbar Expression rbrace { Universal $2 Nothing (Just $4) }
+          | lbrace Args vbar StaticExpression rbrace { Universal $2 Nothing (Just $4) }
 
 -- | Parse the details of an implementation
 Implementation : FunName doubleParens eq Expression { Implement $2 [] [] $1 [] $4 }
@@ -450,6 +450,7 @@
       | doubleEq { StaticEq }
       | eq { Equal }
       | mod { Mod }
+      | percent { Mod }
 
 -- | Optionally parse a function body
 OptExpression : { Nothing }
diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs
--- a/src/Language/ATS/PrettyPrint.hs
+++ b/src/Language/ATS/PrettyPrint.hs
@@ -100,7 +100,7 @@
     pretty LessThanEq    = "<="
     pretty GreaterThanEq = ">="
     pretty StaticEq      = "=="
-    pretty Mod           = "mod"
+    pretty Mod           = "%"
 
 splits :: BinOp -> Bool
 splits Mult       = True
@@ -216,10 +216,17 @@
     pretty (PrfArg a a')    = pretty a <+> "|" <+> pretty a'
     pretty NoArgs           = "FIXME"
 
+squish :: BinOp -> Bool
+squish Add = True
+squish Sub = True
+squish _   = False
+
 instance Pretty StaticExpression where
     pretty = cata a where
         a (StaticValF n)            = pretty n
-        a (StaticBinaryF op se se') = se <> pretty op <> se'
+        a (StaticBinaryF op se se')
+            | squish op = se <> pretty op <> se'
+            | otherwise = se <+> pretty op <+> se'
         a (StaticIntF i)            = pretty i
         a (SifF e e' e'')           = "sif" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''
         a (StaticBoolF True)        = "true"
@@ -292,14 +299,18 @@
     pretty (Implement _ ps [] n ias e) = "implement" <+> foldMap pretty ps </> pretty n <+> prettyArgs ias <+> "=" <$> indent 2 (pretty e)
     pretty (Implement _ ps us n ias e) = "implement" <+> foldMap pretty ps </> pretty n </> foldMap pretty us <+> prettyArgs ias <+> "=" <$> indent 2 (pretty e)
 
+isVal :: Declaration -> Bool
+isVal Val{}   = True
+isVal Var{}   = True
+isVal PrVal{} = True
+isVal _       = False
+
 glue :: Declaration -> Declaration -> Bool
+glue x y
+    | isVal x && isVal y = True
 glue Staload{} Staload{}           = True
 glue Include{} Include{}           = True
 glue ViewTypeDef{} ViewTypeDef{}   = True
-glue Val{} Val{}                   = True
-glue Val{} Var{}                   = True
-glue Var{} Val{}                   = True
-glue Var{} Var{}                   = True
 glue Comment{} _                   = True
 glue (Func _ Fnx{}) (Func _ And{}) = True
 glue _ _                           = False
diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs
--- a/src/Language/ATS/Types.hs
+++ b/src/Language/ATS/Types.hs
@@ -159,7 +159,7 @@
     deriving (Show, Eq, Generic, NFData)
 
 -- | Wrapper for universal quantifiers (refinement types)
-data Universal = Universal { bound :: [Arg], typeU :: Maybe Type, prop :: Maybe Expression }
+data Universal = Universal { bound :: [Arg], typeU :: Maybe Type, prop :: Maybe StaticExpression }
     deriving (Show, Eq, Generic, NFData)
 
 -- | Wrapper for existential quantifiers/types