diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr
index 42e2170..6419c55 100644
--- a/lib/Quox/Parser/Parser.idr
+++ b/lib/Quox/Parser/Parser.idr
@@ -585,22 +585,32 @@ where
     foldr (\(q, x, s), t => Pi q x s t loc) cod $ toDoms (toQty q) doms
 
 
-letIntro : FileName -> Grammar True PQty
+export
+letIntro : FileName -> Grammar True (Maybe PQty)
 letIntro fname =
-      withLoc fname (PQ Zero <$ res "let0")
-  <|> withLoc fname (PQ One  <$ res "let1")
-  <|> withLoc fname (PQ Any  <$ res "letω")
-  <|> do resC "let"
-         qty fname <* needRes "." <|> defLoc fname (PQ One)
+      withLoc fname (Just . PQ Zero <$ res "let0")
+  <|> withLoc fname (Just . PQ One  <$ res "let1")
+  <|> withLoc fname (Just . PQ Any  <$ res "letω")
+  <|> Nothing <$ resC "let"
+
+export
+letBinder : FileName -> Maybe PQty -> Grammar True (PQty, PatVar, PTerm)
+letBinder fname mq = do
+  qty <- the (Grammar False PQty) $ case mq of
+    Just q  => pure q
+    Nothing => qty fname <* mustWork (resC ".") <|> defLoc fname (PQ One)
+  x   <- patVar fname; mustWork (resC "=")
+  rhs <- term fname
+  pure $ (qty, x, rhs)
 
 export
 letTerm : FileName -> Grammar True PTerm
 letTerm fname = withLoc fname $ do
-  qty  <- letIntro fname
-  x    <- patVar fname <* mustWork (resC "=")
-  rhs  <- assert_total term fname <* mustWork (resC "in")
-  body <- assert_total term fname
-  pure $ Let (qty, x, rhs) body
+  qty   <- letIntro fname
+  binds <- sepEndBy1 (res ";") $ assert_total letBinder fname qty
+  mustWork $ resC "in"
+  body  <- assert_total term fname
+  pure $ \loc => foldr (\b, s => Let b s loc) body binds
 
 -- term : FileName -> Grammar True PTerm
 term fname = lamTerm fname
diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr
index dc27730..e1f780a 100644
--- a/tests/Tests/Parser.idr
+++ b/tests/Tests/Parser.idr
@@ -414,12 +414,16 @@ tests = "parser" :- [
   "let" :- [
     parseMatch term "let x = y in z"
       `(Let (PQ One _, PV "x" {}, V "y" {}) (V "z" {}) _),
+    parseMatch term "let x = y; in z"
+      `(Let (PQ One _, PV "x" {}, V "y" {}) (V "z" {}) _),
     parseMatch term "let0 x = y in z"
       `(Let (PQ Zero _, PV "x" {}, V "y" {}) (V "z" {}) _),
     parseMatch term "let1 x = y in z"
       `(Let (PQ One _, PV "x" {}, V "y" {}) (V "z" {}) _),
     parseMatch term "letω x = y in z"
       `(Let (PQ Any _, PV "x" {}, V "y" {}) (V "z" {}) _),
+    parseMatch term "let ω.x = y in z"
+      `(Let (PQ Any _, PV "x" {}, V "y" {}) (V "z" {}) _),
     parseMatch term "let x = y1 y2 in z1 z2"
       `(Let (PQ One _, PV "x" {},
              (App (V "y1" {}) (V "y2" {}) _))
@@ -427,12 +431,27 @@ tests = "parser" :- [
     parseMatch term "let x = a in let y = b in z"
       `(Let (PQ One _, PV "x" {}, V "a" {})
         (Let (PQ One _, PV "y" {}, V "b" {}) (V "z" {}) _) _),
+    parseMatch term "let x = a; y = b in z"
+      `(Let (PQ One _, PV "x" {}, V "a" {})
+        (Let (PQ One _, PV "y" {}, V "b" {}) (V "z" {}) _) _),
+    parseMatch term "letω x = a; y = b in z"
+      `(Let (PQ Any _, PV "x" {}, V "a" {})
+        (Let (PQ Any _, PV "y" {}, V "b" {}) (V "z" {}) _) _),
+    parseMatch term "letω x = a; y = b; in z"
+      `(Let (PQ Any _, PV "x" {}, V "a" {})
+        (Let (PQ Any _, PV "y" {}, V "b" {}) (V "z" {}) _) _),
+    parseMatch term "let ω.x = a; 1.y = b in z"
+      `(Let (PQ Any _, PV "x" {}, V "a" {})
+        (Let (PQ One _, PV "y" {}, V "b" {}) (V "z" {}) _) _),
     parseMatch term "let x = y in z ∷ Z"
       `(Let (PQ One _, PV "x" {}, V "y" {})
           (Ann (V "z" {}) (V "Z" {}) _) _),
     parseMatch term "let x = y in z₁ ≡ z₂ : Z"
       `(Let (PQ One _, PV "x" {}, V "y" {})
-          (Eq (Unused _, V "Z" {}) (V "z₁" {}) (V "z₂" {}) _) _)
+          (Eq (Unused _, V "Z" {}) (V "z₁" {}) (V "z₂" {}) _) _),
+    parseFails term "let1 1.x = y in z",
+    parseFails term "let x = y",
+    parseFails term "let x in z"
   ],
 
   "definitions" :-