diff --git a/lib/Quox/Name.idr b/lib/Quox/Name.idr
index cee177f..03f4271 100644
--- a/lib/Quox/Name.idr
+++ b/lib/Quox/Name.idr
@@ -57,7 +57,7 @@ public export
 record PName where
   constructor MakePName
   mods : Mods
-  base : String
+  base : PBaseName
 %runElab derive "PName" [Eq, Ord]
 
 export %inline
@@ -68,6 +68,10 @@ export %inline
 toPName : Name -> PName
 toPName p = MakePName p.mods $ baseStr p.base
 
+export %inline
+fromPBaseName : PBaseName -> Name
+fromPBaseName = MakeName [<] . UN
+
 export
 Show PName where
   show (MakePName mods base) = concat $ intersperse "." $ toList $ mods :< base
@@ -76,7 +80,7 @@ export Show Name where show = show . toPName
 
 export FromString PName where fromString = MakePName [<]
 
-export FromString Name where fromString = fromPName . fromString
+export FromString Name where fromString = fromPBaseName
 
 
 export
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index f6a0b99..7359c23 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -245,8 +245,8 @@ globalPQty pi = case choose $ isGlobal pi of
 
 
 export
-fromPNameNS : Has (StateL NS Mods) fs => PName -> Eff fs Name
-fromPNameNS name = pure $ addMods !(getAt NS) $ fromPName name
+fromPBaseNameNS : Has (StateL NS Mods) fs => PBaseName -> Eff fs Name
+fromPBaseNameNS name = pure $ addMods !(getAt NS) $ fromPBaseName name
 
 private
 injTC : (Has (StateL DEFS Definitions) fs, Has (Except Error) fs) =>
@@ -259,7 +259,7 @@ fromPDef : (Has (StateL DEFS Definitions) fs,
             Has (Except Error) fs) =>
            PDefinition -> Eff fs NDefinition
 fromPDef (MkPDef qty pname ptype pterm) = do
-  name <- fromPNameNS pname
+  name <- fromPBaseNameNS pname
   qtyGlobal <- globalPQty qty
   let gqty = Element qty qtyGlobal
   let sqty = globalToSubj gqty
diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr
index cc33b4b..139536c 100644
--- a/lib/Quox/Parser/Parser.idr
+++ b/lib/Quox/Parser/Parser.idr
@@ -3,6 +3,7 @@ module Quox.Parser.Parser
 import public Quox.Parser.Lexer
 import public Quox.Parser.Syntax
 
+import Data.Bool
 import Data.Fin
 import Data.Vect
 import public Text.Parser
@@ -18,349 +19,6 @@ Grammar = Core.Grammar () Token
 %hide Core.Grammar
 
 
-export
-res : (str : String) -> (0 _ : IsReserved str) => Grammar True ()
-res str = terminal "expecting \"\{str}\"" $ guard . (== Reserved str)
-
-export
-resC : (str : String) -> (0 _ : IsReserved str) => Grammar True ()
-resC str = do res str; commit
-
-
-parameters {default True commit : Bool}
-  private
-  maybeCommit : Grammar False ()
-  maybeCommit = when commit Core.commit
-
-  export
-  betweenR : {c : Bool} -> (op, cl : String) ->
-             (0 _ : IsReserved op) => (0 _ : IsReserved cl) =>
-             Grammar c a -> Grammar True a
-  betweenR o c p = res o *> maybeCommit *> p <* res c <* maybeCommit
-
-  export
-  parens, bracks, braces : {c : Bool} -> Grammar c a -> Grammar True a
-  parens = betweenR "(" ")"
-  bracks = betweenR "[" "]"
-  braces = betweenR "{" "}"
-
-
-export
-commaSep : {c : Bool} -> Grammar c a -> Grammar False (List a)
-commaSep = sepEndBy (res ",")
-  -- don't commit because of the possible terminating ","
-
-export
-semiSep : {c : Bool} -> Grammar c a -> Grammar False (List a)
-semiSep = sepEndBy (res ";")
-
-export
-commaSep1 : {c : Bool} -> Grammar c a -> Grammar c (List1 a)
-commaSep1 = sepEndBy1 (res ",")
-
-export
-darr : Grammar True ()
-darr = resC "⇒"
-
-
-export
-name : Grammar True PName
-name = terminal "expecting name" $
-  \case Name i => Just i; _ => Nothing
-
-export
-mods : Grammar True Mods
-mods = name <&> \n => n.mods :< n.base
-
-export
-baseName : Grammar True String
-baseName = terminal "expecting unqualified name" $
-  \case Name i => guard (null i.mods) $> i.base
-        _      => Nothing
-
-export
-nat : Grammar True Nat
-nat = terminal "expecting natural number" $
-  \case Nat n => pure n; _ => Nothing
-
-export
-string : Grammar True String
-string = terminal "expecting string literal" $
-  \case Str s => pure s; _ => Nothing
-
-export
-tag : Grammar True String
-tag = terminal "expecting tag constructor" $
-  \case Tag t => pure t; _ => Nothing
-
-export
-bareTag : Grammar True String
-bareTag = string <|> [|toDotsP name|]
-
-export
-universe : Grammar True PUniverse
-universe = terminal "expecting type universe" $
-  \case TYPE u => Just u; _ => Nothing
-
-export
-bname : Grammar True BName
-bname = Nothing <$ res "_"
-    <|> [|Just baseName|]
-
-export
-dimConst : Grammar True DimConst
-dimConst = terminal "expecting 0 or 1" $
-  \case Nat 0 => Just Zero; Nat 1 => Just One; _ => Nothing
-
-export
-qty : Grammar True Qty
-qty = terminal "expecting quantity" $
-  \case Nat 0 => Just Zero; Nat 1 => Just One; Reserved "ω" => Just Any
-        _ => Nothing
-
-export
-zero : Grammar True ()
-zero = terminal "expecting 0" $ guard . (== Nat 0)
-
-
-public export
-AllReserved : List (a, String) -> Type
-AllReserved = foldr (\x, ps => (IsReserved $ snd x, ps)) ()
-
-export
-symbols : (lst : List (a, String)) -> (0 _ : AllReserved lst) =>
-          Grammar True a
-symbols []                 = fail "no symbols found"
-symbols [(x, str)]         = x <$ res str
-symbols ((x, str) :: rest) = x <$ res str <|> symbols rest
-
-export
-symbolsC : (lst : List (a, String)) -> (0 _ : AllReserved lst) =>
-           Grammar True a
-symbolsC lst = symbols lst <* commit
-
-
-private covering
-qtys : Grammar False (List Qty)
-qtys = option [] [|toList $ some qty <* res "."|]
-
-
-export
-dim : Grammar True PDim
-dim = [|V baseName|] <|> [|K dimConst|]
-
-private
-0 PBinderHead : Nat -> Type
-PBinderHead n = (Vect n Qty, BName, PTerm)
-
-private
-toVect : List a -> (n ** Vect n a)
-toVect []        = (_ ** [])
-toVect (x :: xs) = (_ ** x :: snd (toVect xs))
-
-
-private
-lamIntro : Grammar True (BName -> PTerm -> PTerm)
-lamIntro = symbolsC [(Lam, "λ"), (DLam, "δ")]
-
-private covering
-caseIntro : Grammar True Qty
-caseIntro = symbols [(Zero, "case0"), (One, "case1"), (Any, "caseω")]
-        <|> resC "case" *>
-              (qty <* resC "." <|>
-               fatalError {c = True} "missing quantity on 'case'")
-
-private
-optNameBinder : Grammar False BName
-optNameBinder = [|join $ optional $ bname <* darr|]
-
-mutual
-  export covering
-  term : Grammar True PTerm
-  term = lamTerm <|> caseTerm <|> coeTerm <|> compTerm <|> bindTerm <|> annTerm
-
-  private covering
-  lamTerm : Grammar True PTerm
-  lamTerm = flip . foldr <$> lamIntro <*> some bname <* darr <*> term
-
-  private covering
-  caseTerm : Grammar True PTerm
-  caseTerm =
-    [|Case caseIntro term
-           (resC "return" *> optBinderTerm)
-           (resC "of"     *> caseBody)|]
-
-  private covering
-  coeTerm : Grammar True PTerm
-  coeTerm = resC "coe" *> [|Coe typeLine dimArg dimArg aTerm|]
-
-  private covering
-  compTerm : Grammar True PTerm
-  compTerm = resC "comp" *> do
-    head <- [|Comp typeLine dimArg dimArg aTerm dimArg|]
-    uncurry head <$> compBody
-  where
-    compBranch : Grammar True (DimConst, BName, PTerm)
-    compBranch = [|(,,) dimConst bname (resC "⇒" *> term)|]
-
-    zeroOne : (DimConst, a) -> (DimConst, a) -> Grammar False (a, a)
-    zeroOne (Zero, x) (One,  y) = pure (x, y)
-    zeroOne (One,  x) (Zero, y) = pure (y, x)
-    zeroOne _ _ = fatalError "body of comp needs one 0 branch and one 1 branch"
-
-    compBody : Grammar True ((BName, PTerm), (BName, PTerm))
-    compBody = braces $ do
-      et0 <- compBranch <* resC ";"
-      et1 <- compBranch <* optional (resC ";")
-      zeroOne et0 et1
-
-  private covering
-  caseBody : Grammar True PCaseBody
-  caseBody = braces $
-        [|CasePair (pairPat <* darr) (term <* optSemi)|]
-    <|> [|CaseBox (bracks bname <* darr) (term <* optSemi)|]
-    <|> CaseNat <$> zeroCase <* resC ";" <*> succCase <* optSemi
-    <|> flip CaseNat <$> succCase <* resC ";" <*> zeroCase <* optSemi
-    <|> [|CaseEnum $ semiSep [|MkPair tag (darr *> term)|]|]
-  where
-    optSemi = optional $ res ";"
-    pairPat = parens [|MkPair bname (resC "," *> bname)|]
-
-    zeroCase : Grammar True PTerm
-    zeroCase = (resC "zero" <|> zero) *> darr *> term
-
-    succCase : Grammar True (BName, Qty, BName, PTerm)
-    succCase = do
-      resC "succ"
-      n  <- bname
-      ih <- option (Zero, Nothing) $
-        resC "," *> [|MkPair qty (resC "." *> bname)|]
-      rhs <- darr *> term
-      pure $ (n, fst ih, snd ih, rhs)
-
-  private covering
-  bindTerm : Grammar True PTerm
-  bindTerm = pi <|> sigma
-  where
-    binderHead =
-      parens {commit = False} [|MkPair (some bname) (resC ":" *> term)|]
-
-    pi, sigma : Grammar True PTerm
-    pi = [|makePi (qty <* res ".") domain (resC "→" *> term)|]
-    where
-      makePi : Qty -> (List1 BName, PTerm) -> PTerm -> PTerm
-      makePi q (xs, s) t = foldr (\x => Pi q x s) t xs
-      domain = binderHead <|> [|(Nothing ::: [],) aTerm|]
-
-    sigma = [|makeSigma binderHead (resC "×" *> annTerm)|]
-    where
-      makeSigma : (List1 BName, PTerm) -> PTerm -> PTerm
-      makeSigma (xs, s) t = foldr (\x => Sig x s) t xs
-
-  private covering
-  annTerm : Grammar True PTerm
-  annTerm = [|annotate infixEqTerm (optional $ resC "∷" *> term)|]
-  where annotate s a = maybe s (s :#) a
-
-  private covering
-  infixEqTerm : Grammar True PTerm
-  infixEqTerm = do
-    l <- infixTimesTerm
-    rty <- optional [|MkPair (resC "≡" *> term) (resC ":" *> infixTimesTerm)|]
-    pure $ maybe l (\rty => Eq (Nothing, snd rty) l (fst rty)) rty
-
-  private covering
-  infixTimesTerm : Grammar True PTerm
-  infixTimesTerm = foldr1 (Sig Nothing) <$> sepBy1 (resC "×") appTerm
-
-  private covering
-  appTerm : Grammar True PTerm
-  appTerm = resC "★"    *> [|TYPE nat|]
-        <|> resC "Eq"   *> [|Eq typeLine aTerm aTerm|]
-        <|> resC "succ" *> [|Succ aTerm|]
-        <|> [|apply aTerm (many appArg)|]
-  where
-    data PArg = TermArg PTerm | DimArg PDim
-
-    appArg : Grammar True PArg
-    appArg = [|DimArg dimArg|] <|> [|TermArg aTerm|]
-
-    apply : PTerm -> List PArg -> PTerm
-    apply = foldl apply1 where
-      apply1 : PTerm -> PArg -> PTerm
-      apply1 f (TermArg x) = f :@ x
-      apply1 f (DimArg  p) = f :% p
-
-  private covering
-  typeLine : Grammar True (BName, PTerm)
-  typeLine = bracks optBinderTerm
-
-  private covering
-  dimArg : Grammar True PDim
-  dimArg = resC "@" *> dim
-
-  private covering
-  aTerm : Grammar True PTerm
-  aTerm = [|Enum $ braces $ commaSep bareTag|]
-      <|> foldr1 Pair <$> parens (commaSep1 term)
-      <|> boxTerm
-      <|> [|TYPE universe|]
-      <|> Nat  <$ resC "ℕ"
-      <|> Zero <$ resC "zero"
-      <|> [|fromNat nat|]
-      <|> [|V name|]
-      <|> [|Tag tag|]
-
-  private covering
-  boxTerm : Grammar True PTerm
-  boxTerm = bracks $
-        [|BOX (qty <* resC ".") term|]
-    <|> [|Box term|]
-
-  private covering
-  optBinderTerm : Grammar True (BName, PTerm)
-  optBinderTerm = [|MkPair optNameBinder term|]
-
-
-export covering
-defIntro : Grammar True Qty
-defIntro = symbols [(Zero, "def0"), (Any, "defω")]
-       <|> resC "def" *> option Any (qty <* resC ".")
-
-skipSemis : Grammar False ()
-skipSemis = ignore $ many $ resC ";"
-
-export covering
-definition : Grammar True PDefinition
-definition =
-  [|MkPDef defIntro name (optional (resC ":" *> term)) (resC "=" *> term)|]
-
-export
-load : Grammar True String
-load = resC "load" *> string
-
-mutual
-  export covering
-  namespace_ : Grammar True PNamespace
-  namespace_ =
-    [|MkPNamespace (resC "namespace" *> mods)
-        (braces $ many $ decl <* skipSemis)|]
-
-  export covering
-  decl : Grammar True PDecl
-  decl = [|PDef definition|]
-     <|> [|PNs  namespace_|]
-
-export covering
-topLevel : Grammar True PTopLevel
-topLevel = [|PLoad load|]
-       <|> [|PD    decl|]
-
-export covering
-input : Grammar False (List PTopLevel)
-input = skipSemis *> many (topLevel <* skipSemis)
-
-
 public export
 data Error =
     LexError   Lexer.Error
@@ -374,10 +32,446 @@ lexParseWith grm input = do
   toks <- mapFst LexError $ lex input
   bimap ParseError fst $ parse (grm <* eof) toks
 
-export covering %inline
-lexParseInput : String -> Either Error (List PTopLevel)
-lexParseInput = lexParseWith input
 
-export covering %inline
+||| reserved token, like punctuation or keywords etc
+export
+res : (str : String) -> (0 _ : IsReserved str) => Grammar True ()
+res str = terminal "expected \"\{str}\"" $ guard . (== Reserved str)
+
+||| optional reserved token, e.g. trailing comma
+export
+optRes : (str : String) -> (0 _ : IsReserved str) => Grammar False ()
+optRes str = ignore $ optional $ res str
+
+||| reserved token, then commit
+export
+resC : (str : String) -> (0 _ : IsReserved str) => Grammar True ()
+resC str = do res str; commit
+
+||| reserved token or fatal error
+export
+needRes : (str : String) -> (0 _ : IsReserved str) => Grammar True ()
+needRes str = resC str <|> fatalError "expected \"\{str}\""
+
+
+private
+terminalMatchN_ : String -> List (TTImp, TTImp) -> Elab (Grammar True a)
+terminalMatchN_ what matches = do
+  func <- check $ lam (lambdaArg `{x}) $
+    iCase `(x) implicitFalse $
+    map (\(l, r) => patClause l `(Just ~(r))) matches ++
+      [patClause `(_) `(Nothing)]
+  pure $ terminal "expected \{what}" func
+
+private %macro
+terminalMatchN : String -> List (TTImp, TTImp) -> Elab (Grammar True a)
+terminalMatchN = terminalMatchN_
+
+private %macro
+terminalMatch : String -> TTImp -> TTImp -> Elab (Grammar True a)
+terminalMatch what l r = terminalMatchN_ what [(l, r)]
+
+||| tag without leading `'`
+export
+bareTag : Grammar True TagVal
+bareTag = terminalMatchN "bare tag" [(`(Name t), `(show t)), (`(Str s), `(s))]
+
+||| tag with leading quote
+export
+tag : Grammar True TagVal
+tag = terminalMatch "tag" `(Tag t) `(t)
+
+||| natural number
+export
+nat : Grammar True Nat
+nat = terminalMatch "natural number" `(Nat n) `(n)
+
+||| string literal
+export
+strLit : Grammar True String
+strLit = terminalMatch "string literal" `(Str s) `(s)
+
+||| single-token universe, like ★₀ or Type1
+export
+universe1 : Grammar True Universe
+universe1 = terminalMatch "universe" `(TYPE u) `(u)
+
+||| possibly-qualified name
+export
+qname : Grammar True PName
+qname = terminalMatch "name" `(Name n) `(n)
+
+||| unqualified name
+export
+baseName : Grammar True PBaseName
+baseName = terminalMatch "unqualified name" `(Name (MakePName [<] b)) `(b)
+
+||| dimension constant (0 or 1)
+export
+dimConst : Grammar True DimConst
+dimConst = terminalMatchN "dimension constant"
+  [(`(Nat 0), `(Zero)), (`(Nat 1), `(One))]
+
+||| quantity (0, 1, or ω)
+export
+qty : Grammar True Qty
+qty = terminalMatchN "quantity"
+  [(`(Nat 0), `(Zero)), (`(Nat 1), `(One)), (`(Reserved "ω"), `(Any))]
+
+
+||| pattern var (unqualified name or _)
+export
+patVar : Grammar True BName
+patVar = [|Just baseName|] <|> Nothing <$ res "_"
+
+
+||| dimension (without `@` prefix)
+export
+dim : Grammar True PDim
+dim = [|K dimConst|] <|> [|V baseName|]
+
+||| dimension argument (with @)
+export
+dimArg : Grammar True PDim
+dimArg = resC "@" *> mustWork dim
+
+
+delim : (o, c : String) -> (0 _ : IsReserved o) => (0 _ : IsReserved c) =>
+        {k : Bool} -> Grammar k a -> Grammar True a
+delim o c p = resC o *> p <* needRes c
+
+-- this stuff is Like This (rather than just being delim + sepEndBy{1})
+-- so that it checks for the close bracket before trying another list element,
+-- giving (imo) a better error
+parameters (o, c, s : String)
+           {auto 0 _ : IsReserved o} {auto 0 _ : IsReserved c}
+           {auto 0 _ : IsReserved s}
+           (p : Grammar True a)
+  private
+  dsBeforeDelim, dsAfterDelim : Grammar True (List a)
+  dsBeforeDelim = [] <$ resC c <|> resC s *> assert_total dsAfterDelim
+  dsAfterDelim  = [] <$ resC c <|> [|p :: assert_total dsBeforeDelim|]
+
+  export
+  delimSep1 : Grammar True (List1 a)
+  delimSep1 = resC o *> [|p ::: dsBeforeDelim|]
+
+  export
+  delimSep : Grammar True (List a)
+  delimSep = resC o *> dsAfterDelim
+
+
+||| enum type, e.g. `{a, b, c.d, "e f g"}`
+export
+enumType : Grammar True (List TagVal)
+enumType = delimSep "{" "}" "," bareTag
+
+||| e.g. `case` or `case 1.`
+export
+caseIntro : Grammar True Qty
+caseIntro =
+      Zero <$ res "case0"
+  <|> One  <$ res "case1"
+  <|> Any  <$ res "caseω"
+  <|> delim "case" "." qty
+
+export
+qtyPatVar : Grammar True (Qty, BName)
+qtyPatVar = [|(,) qty (needRes "." *> patVar)|]
+
+
+public export
+data PCasePat =
+    PPair BName BName
+  | PTag  TagVal
+  | PZero
+  | PSucc BName Qty BName
+  | PBox  BName
+%runElab derive "PCasePat" [Eq, Ord, Show]
+
+public export
+PCaseArm : Type
+PCaseArm = (PCasePat, PTerm)
+
+||| either `zero` or `0`
+export
+zeroPat : Grammar True ()
+zeroPat = resC "zero" <|> terminal "expected '0'" (guard . (== Nat 0))
+
+export
+casePat : Grammar True PCasePat
+casePat =
+      delim "(" ")" [|PPair patVar (needRes "," *> patVar)|]
+  <|> [|PTag tag|]
+  <|> PZero <$ zeroPat
+  <|> do p  <- resC "succ" *> patVar
+         ih <- option (Zero, Nothing) $ resC "," *> qtyPatVar
+         pure $ PSucc p (fst ih) (snd ih)
+  <|> delim "[" "]" [|PBox patVar|]
+  <|> fatalError "invalid pattern"
+
+export
+checkCaseArms : List PCaseArm -> Grammar False PCaseBody
+checkCaseArms [] =
+  pure $ CaseEnum []
+checkCaseArms ((PPair x y, rhs) :: rest) = do
+  let [] = rest | _ => fatalError "unexpected pattern after pair"
+  pure $ CasePair (x, y) rhs
+checkCaseArms ((PTag tag, rhs1) :: rest) = do
+  let rest = for rest $ \case
+        (PTag tag, rhs) => Just (tag, rhs)
+        _               => Nothing
+  maybe (fatalError "expected all patterns to be tags")
+        (pure . CaseEnum . ((tag, rhs1) ::)) rest
+checkCaseArms ((PZero, rhs1) :: rest) = do
+  let [(PSucc p q ih, rhs2)] = rest
+    | _ => fatalError "expected succ pattern after zero"
+  pure $ CaseNat rhs1 (p, q, ih, rhs2)
+checkCaseArms ((PSucc p q ih, rhs1) :: rest) = do
+  let [(PZero, rhs2)] = rest
+    | _ => fatalError "expected zero pattern after succ"
+  pure $ CaseNat rhs2 (p, q, ih, rhs1)
+checkCaseArms ((PBox x, rhs) :: rest) = do
+  let [] = rest | _ => fatalError "unexpected pattern after box"
+  pure $ CaseBox x rhs
+
+
+mutual
+  export covering
+  typeLine : Grammar True (BName, PTerm)
+  typeLine = do
+    resC "["
+    mustWork $ do
+      i <- option Nothing $ patVar <* resC "⇒"
+      t <- term <* needRes "]"
+      pure (i, t)
+
+  ||| argument/atomic term: single-token terms, or those with delimiters e.g.
+  ||| `[t]`
+  export covering
+  termArg : Grammar True PTerm
+  termArg = [|TYPE universe1|]
+        <|> [|Enum enumType|]
+        <|> [|Tag tag|]
+        <|> boxTerm
+        <|> Nat  <$ res "ℕ"
+        <|> Zero <$ res "zero"
+        <|> [|fromNat nat|]
+        <|> [|V qname|]
+        <|> tupleTerm
+
+  ||| box term `[t]` or type `[π.A]`
+  export covering
+  boxTerm : Grammar True PTerm
+  boxTerm = do
+    res "["; commit
+    q <- optional $ qty  <* res "."
+    t <- mustWork $ term <* needRes "]"
+    pure $ maybe (Box t) (\q => BOX q t) q
+
+  ||| tuple term like `(a, b)`, or parenthesised single term.
+  ||| allows terminating comma. more than two elements are nested on the right:
+  ||| `(a, b, c, d) = (a, (b, (c, d)))`.
+  export covering
+  tupleTerm : Grammar True PTerm
+  tupleTerm = foldr1 Pair <$> delimSep1 "(" ")" "," term
+
+  ||| application term `f x @y z`, or other terms that look like application
+  ||| like `succ` or `coe`.
+  export covering
+  appTerm : Grammar True PTerm
+  appTerm = coeTerm
+        <|> compTerm
+        <|> splitUniverseTerm
+        <|> eqTerm
+        <|> succTerm
+        <|> normalAppTerm
+
+  export covering
+  coeTerm : Grammar True PTerm
+  coeTerm = resC "coe" *> mustWork [|Coe typeLine dimArg dimArg termArg|]
+
+  export covering
+  compTerm : Grammar True PTerm
+  compTerm = do
+    resC "comp"
+    mustWork $ do
+      a <- typeLine
+      p <- dimArg;  q <- dimArg
+      s <- termArg; r <- dimArg
+      needRes "{"
+      s0 <- compBranch; needRes ";"
+      s1 <- compBranch; optRes  ";"
+      needRes "}"
+      case (fst s0, fst s1) of
+        (Zero, One)  => pure $ Comp a p q s r (snd s0) (snd s1)
+        (One,  Zero) => pure $ Comp a p q s r (snd s1) (snd s0)
+        (_,    _)    =>
+          fatalError "body of 'comp' needs one 0 case and one 1 case"
+
+  export covering
+  compBranch : Grammar True (DimConst, BName, PTerm)
+  compBranch = [|(,,) dimConst patVar (needRes "⇒" *> term)|]
+
+  export covering
+  splitUniverseTerm : Grammar True PTerm
+  splitUniverseTerm = resC "★" *> mustWork [|TYPE nat|]
+
+  export covering
+  eqTerm : Grammar True PTerm
+  eqTerm = resC "Eq" *> mustWork [|Eq typeLine termArg termArg|]
+
+  export covering
+  succTerm : Grammar True PTerm
+  succTerm = resC "succ" *> mustWork [|Succ termArg|]
+
+  export covering
+  normalAppTerm : Grammar True PTerm
+  normalAppTerm = foldl ap <$> termArg <*> many anyArg
+  where ap : PTerm -> Either PDim PTerm -> PTerm
+        ap f (Left  p) = f :% p
+        ap f (Right s) = f :@ s
+
+  ||| a dimension argument with an `@` prefix, or
+  ||| a term argument with no prefix
+  export covering
+  anyArg : Grammar True (Either PDim PTerm)
+  anyArg = dimArg <||> termArg
+
+  export covering
+  term : Grammar True PTerm
+  term = lamTerm
+     <|> caseTerm
+     <|> piTerm
+     <|> sigmaTerm
+
+  export covering
+  lamTerm : Grammar True PTerm
+  lamTerm = do
+    k <- DLam <$ res "δ" <|> Lam <$ res "λ"
+    mustWork $ do
+      xs   <- some patVar; needRes "⇒"
+      body <- term;        commit
+      pure $ foldr k body xs
+
+  export covering
+  piTerm : Grammar True PTerm
+  piTerm = do
+    q   <- qty;      resC "."
+    dom <- piBinder; needRes "→"
+    cod <- term;     commit
+    pure $ foldr (\x => Pi q x (snd dom)) cod (fst dom)
+  where
+    piBinder : Grammar True (List1 BName, PTerm)
+    piBinder = properBinders <|> [|(singleton Nothing,) termArg|]
+
+  -- [todo] fix the backtracking in e.g. (F x y z × B)
+  export covering
+  properBinders : Grammar True (List1 BName, PTerm)
+  properBinders = do
+    res "("
+    xs <- some patVar; resC ":"
+    t  <- term;        needRes ")"
+    pure (xs, t)
+
+  export covering
+  sigmaTerm : Grammar True PTerm
+  sigmaTerm =
+        (properBinders >>= continueDep)
+    <|> (annTerm       >>= continueNondep)
+  where
+    continueDep : (List1 BName, PTerm) -> Grammar True PTerm
+    continueDep (names, dom) = do
+      cod <- needRes "×" *> sigmaTerm
+      pure $ foldr (\x => Sig x dom) cod names
+    continueNondep : PTerm -> Grammar False PTerm
+    continueNondep dom = do
+      rest <- optional $ resC "×" *> sepBy1 (res "×") annTerm
+      Core.pure $ foldr1 (Sig Nothing) $ dom ::: maybe [] forget rest
+
+  export covering
+  annTerm : Grammar True PTerm
+  annTerm = do
+    tm <- infixEqTerm; commit
+    ty <- optional $ res "∷" *> term
+    pure $ maybe tm (tm :#) ty
+
+  export covering
+  infixEqTerm : Grammar True PTerm
+  infixEqTerm = do
+    l <- appTerm; commit
+    rest <- optional $ res "≡" *> [|(,) term (needRes ":" *> appTerm)|]
+    pure $ maybe l (\rest => Eq (Nothing, snd rest) l (fst rest)) rest
+
+  export covering
+  caseTerm : Grammar True PTerm
+  caseTerm = do
+    qty <- caseIntro; commit
+    head <- mustWork term; needRes "return"
+    ret  <- mustWork [|(,) (option Nothing $ patVar <* resC "⇒") term|]
+    needRes "of"
+    body <- mustWork caseBody
+    pure $ Case qty head ret body
+
+  export covering
+  caseBody : Grammar True PCaseBody
+  caseBody = delimSep "{" "}" ";" caseArm >>= checkCaseArms
+
+  export covering
+  caseArm : Grammar True PCaseArm
+  caseArm = [|(,) casePat (needRes "⇒" *> term)|]
+
+
+||| `def` alone means `defω`
+export
+defIntro : Grammar True Qty
+defIntro = Zero <$ resC "def0"
+       <|> Any  <$ resC "defω"
+       <|> resC "def" *> option Any (qty <* needRes ".")
+
+mutual
+  export covering
+  definition : Grammar True PDefinition
+  definition = do
+    qty  <- defIntro
+    name <- baseName
+    type <- optional $ resC ":" *> mustWork term
+    term <- needRes "=" *> mustWork term
+    optRes ";"
+    pure $ MkPDef {qty, name, type, term}
+
+  export covering
+  namespace_ : Grammar True PNamespace
+  namespace_ = do
+    ns    <- resC "namespace" *> qname; needRes "{"
+    decls <- nsInner; optRes ";"
+    pure $ MkPNamespace (ns.mods :< ns.base) decls
+  where
+    nsInner : Grammar True (List PDecl)
+    nsInner = [] <$ resC "}"
+          <|> [|(decl <* commit) :: nsInner|]
+
+  export covering
+  decl : Grammar True PDecl
+  decl = [|PDef definition|] <|> [|PNs namespace_|]
+
+export covering
+load : Grammar True String
+load = resC "load" *> mustWork strLit <* optRes ";"
+
+export covering
+topLevel : Grammar True PTopLevel
+topLevel = [|PLoad load|] <|> [|PD decl|]
+
+export covering
+input : Grammar False (List PTopLevel)
+input = [] <$ eof
+    <|> [|(topLevel <* commit) :: input|]
+
+export covering
 lexParseTerm : String -> Either Error PTerm
 lexParseTerm = lexParseWith term
+
+export covering
+lexParseInput : String -> Either Error (List PTopLevel)
+lexParseInput = lexParseWith input
diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr
index cdb3ed4..0c33ff5 100644
--- a/lib/Quox/Parser/Syntax.idr
+++ b/lib/Quox/Parser/Syntax.idr
@@ -11,11 +11,11 @@ import Derive.Prelude
 
 
 public export
-0 BName : Type
+BName : Type
 BName = Maybe String
 
 public export
-0 PUniverse : Type
+PUniverse : Type
 PUniverse = Nat
 
 namespace PDim
@@ -37,7 +37,7 @@ namespace PTerm
 
       | Sig BName PTerm PTerm
       | Pair PTerm PTerm
-      | Case Qty PTerm (BName, PTerm) (PCaseBody)
+      | Case Qty PTerm (BName, PTerm) PCaseBody
 
       | Enum (List TagVal)
       | Tag TagVal
@@ -74,7 +74,7 @@ public export
 record PDefinition where
   constructor MkPDef
   qty  : Qty
-  name : PName
+  name : PBaseName
   type : Maybe PTerm
   term : PTerm
 %name PDefinition def
diff --git a/syntax.ebnf b/syntax.ebnf
index c17444f..685e923 100644
--- a/syntax.ebnf
+++ b/syntax.ebnf
@@ -24,7 +24,7 @@ dim arg = "@", dim.
 
 pat var = NAME | "_".
 
-term = lambda | case | pi | sigma.
+term = lambda | case | pi | sigma | ann.
 
 lambda = ("λ" | "δ"), {pat var}+, "⇒", term.
 
@@ -61,12 +61,12 @@ comp        = "comp", type line, dim arg, dim arg, term arg, dim arg, comp body.
 comp body   = "{", comp branch, ";", comp branch, [";"], "}".
 comp branch = dim const, name, "⇒", term.
 
-term arg = "{", {BARE TAG}, "}"
+term arg = UNIVERSE
+         | "{", {BARE TAG / ","}, [","], "}"
          | TAG
-         | "(", {term / ","}+, ")"
          | "[", [qty, "."], term, "]"
-         | UNIVERSE
          | "ℕ"
          | "zero"
          | NAT
-         | QNAME.
+         | QNAME
+         | "(", {term / ","}+, [","], ")".
diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr
index 316b8d0..0889997 100644
--- a/tests/Tests/Parser.idr
+++ b/tests/Tests/Parser.idr
@@ -53,18 +53,18 @@ parameters {c : Bool} {auto _ : Show a} (grm : Grammar c a)
 export
 tests : Test
 tests = "parser" :- [
-  "bound names" :- [
-    parsesAs bname "_" Nothing,
-    parsesAs bname "F" (Just "F"),
-    parseFails bname "a.b.c"
+  "pattern vars" :- [
+    parsesAs patVar "_" Nothing,
+    parsesAs patVar "F" (Just "F"),
+    parseFails patVar "a.b.c"
   ],
 
   "names" :- [
-    parsesAs name "x"
+    parsesAs qname "x"
       (MakePName [<] "x"),
-    parsesAs name "Data.String.length"
+    parsesAs qname "Data.String.length"
       (MakePName [< "Data", "String"] "length"),
-    parseFails name "_"
+    parseFails qname "_"
   ],
 
   "dimensions" :- [
@@ -219,9 +219,14 @@ tests = "parser" :- [
     parsesAs term "f x y ≡ g y z : A B C" $
       Eq (Nothing, V "A" :@ V "B" :@ V "C")
          (V "f" :@ V "x" :@ V "y") (V "g" :@ V "y" :@ V "z"),
-    parsesAs term "A × B ≡ A' × B' : ★₁" $
+    parsesAs term "(A × B) ≡ (A' × B') : ★₁" $
       Eq (Nothing, TYPE 1)
          (Sig Nothing (V "A") (V "B")) (Sig Nothing (V "A'") (V "B'")),
+    note "A × (B ≡ A' × B' : ★₁)",
+    parsesAs term "A × B ≡ A' × B' : ★₁" $
+      Sig Nothing (V "A") $
+        Eq (Nothing, TYPE 1)
+           (V "B") (Sig Nothing (V "A'") (V "B'")),
     parseFails term "Eq",
     parseFails term "Eq s t",
     parseFails term "s ≡ t",
@@ -233,7 +238,9 @@ tests = "parser" :- [
     parsesAs term "Nat" Nat,
     parsesAs term "zero" Zero,
     parsesAs term "succ n" (Succ $ V "n"),
-    parsesAs term "3" (Succ (Succ (Succ Zero))),
+    parsesAs term "3" (fromNat 3),
+    parsesAs term "succ (succ 5)" (fromNat 7),
+    parseFails term "succ succ 5",
     parseFails term "succ"
   ],
 
@@ -245,6 +252,28 @@ tests = "parser" :- [
     parsesAs term "[1]" $ Box (Succ Zero)
   ],
 
+  "coe" :- [
+    parsesAs term "coe [A] @p @q x" $
+      Coe (Nothing, V "A") (V "p") (V "q") (V "x"),
+    parsesAs term "coe [i ⇒ A] @p @q x" $
+      Coe (Just "i", V "A") (V "p") (V "q") (V "x"),
+    parseFails term "coe [A] @p @q",
+    parseFails term "coe A @p @q x",
+    parseFails term "coe [i ⇒ A] @p q x"
+  ],
+
+  "comp" :- [
+    parsesAs term "comp [A] @p @q s @r { 0 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁ }" $
+      Comp (Nothing, V "A") (V "p") (V "q") (V "s") (V "r")
+        (Just "𝑗", V "s₀") (Just "𝑘", V "s₁"),
+    parsesAs term "comp [A] @p @q s @r { 1 𝑗 ⇒ s₀; 0 𝑘 ⇒ s₁; }" $
+      Comp (Nothing, V "A") (V "p") (V "q") (V "s") (V "r")
+        (Just "𝑘", V "s₁") (Just "𝑗", V "s₀"),
+    parseFails term "comp [A] @p @q s @r { 1 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁; }",
+    parseFails term "comp [A] @p @q s @r { 0 𝑗 ⇒ s₀ }",
+    parseFails term "comp [A] @p @q s @r { }"
+  ],
+
   "case" :- [
     parsesAs term
       "case1 f s return x ⇒ A x of { (l, r) ⇒ add l r }" $
@@ -310,11 +339,8 @@ tests = "parser" :- [
     parsesAs input "def0 A : ★₀ = {} def0 B : ★₁ = A" $
       [PD $ PDef $ MkPDef Zero "A" (Just $ TYPE 0) (Enum []),
        PD $ PDef $ MkPDef Zero "B" (Just $ TYPE 1) (V "A")],
-    parsesAs input "def0 A : ★₀ = {};;; def0 B : ★₁ = A" $
-      [PD $ PDef $ MkPDef Zero "A" (Just $ TYPE 0) (Enum []),
-       PD $ PDef $ MkPDef Zero "B" (Just $ TYPE 1) (V "A")],
     parsesAs input "" [] {label = "[empty input]"},
-    parsesAs input ";;;;;;;;;;;;;;;;;;;;;;;;;;" [],
+    parseFails input ";;;;;;;;;;;;;;;;;;;;;;;;;;",
     parsesAs input "namespace a {}" [PD $ PNs $ MkPNamespace [< "a"] []],
     parsesAs input "namespace a.b.c {}"
       [PD $ PNs $ MkPNamespace [< "a", "b", "c"] []],