diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr
index 139536c..952fd76 100644
--- a/lib/Quox/Parser/Parser.idr
+++ b/lib/Quox/Parser/Parser.idr
@@ -189,10 +189,6 @@ data PCasePat =
   | PBox  BName
 %runElab derive "PCasePat" [Eq, Ord, Show]
 
-public export
-PCaseArm : Type
-PCaseArm = (PCasePat, PTerm)
-
 ||| either `zero` or `0`
 export
 zeroPat : Grammar True ()
@@ -210,6 +206,174 @@ casePat =
   <|> delim "[" "]" [|PBox patVar|]
   <|> fatalError "invalid pattern"
 
+
+export covering
+term : Grammar True PTerm
+
+export covering
+typeLine : Grammar True (BName, PTerm)
+typeLine = do
+  resC "["
+  mustWork $ do
+    i <- option Nothing $ patVar <* resC "⇒"
+    t <- term <* needRes "]"
+    pure (i, t)
+
+||| 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
+
+||| 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
+
+export covering
+coeTerm : Grammar True PTerm
+coeTerm = resC "coe" *> mustWork [|Coe typeLine dimArg dimArg termArg|]
+
+export covering
+compBranch : Grammar True (DimConst, BName, PTerm)
+compBranch = [|(,,) dimConst patVar (needRes "⇒" *> term)|]
+
+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
+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|]
+
+||| 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
+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
+
+||| 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
+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
+annTerm : Grammar True PTerm
+annTerm = do
+  tm <- infixEqTerm; commit
+  ty <- optional $ res "∷" *> term
+  pure $ maybe tm (tm :#) ty
+
+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
+
+-- [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
+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|]
+
+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
+
+
+public export
+PCaseArm : Type
+PCaseArm = (PCasePat, PTerm)
+
 export
 checkCaseArms : List PCaseArm -> Grammar False PCaseBody
 checkCaseArms [] =
@@ -235,191 +399,29 @@ checkCaseArms ((PBox x, rhs) :: rest) = do
   let [] = rest | _ => fatalError "unexpected pattern after box"
   pure $ CaseBox x rhs
 
+export covering
+caseArm : Grammar True PCaseArm
+caseArm = [|(,) casePat (needRes "⇒" *> term)|]
 
-mutual
-  export covering
-  typeLine : Grammar True (BName, PTerm)
-  typeLine = do
-    resC "["
-    mustWork $ do
-      i <- option Nothing $ patVar <* resC "⇒"
-      t <- term <* needRes "]"
-      pure (i, t)
+export covering
+caseBody : Grammar True PCaseBody
+caseBody = delimSep "{" "}" ";" caseArm >>= checkCaseArms
 
-  ||| 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
+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
 
-  ||| 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)|]
+term = lamTerm
+   <|> caseTerm
+   <|> piTerm
+   <|> sigmaTerm
 
 
 ||| `def` alone means `defω`
@@ -429,31 +431,32 @@ 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
 
-  export covering
-  decl : Grammar True PDecl
-  decl = [|PDef definition|] <|> [|PNs namespace_|]
+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|]
+
+decl = [|PDef definition|] <|> [|PNs namespace_|]
 
 export covering
 load : Grammar True String