diff --git a/TODO.md b/TODO.md
index 94f81a7..76b1274 100644
--- a/TODO.md
+++ b/TODO.md
@@ -3,7 +3,7 @@
 
 - [ ] Add icit to Lam (see `check` for details)
 - [ ] TCO? Probably needed in browser, since v8 doesn't do it. bun and JavaScriptCore do support it.
-- [ ] deconstructing `let`
+- [x] deconstructing `let` (and do arrows)
 - [x] Fix string printing to be js instead of weird Idris strings
 - [ ] make $ special
   - Makes inference easier, cleaner output, and allows `foo $ \ x => ...`
@@ -14,6 +14,7 @@
   - Idris needs help with the case tree to keep code size down, do it in stages, one dcon at a time.
 - [ ] Strategy to avoid three copies of `Prelude.newt` in this source tree
 - [ ] `mapM` needs inference help when scrutinee (see Day2.newt)
+  - Meta hasn't been solved yet. It's Normal, but maybe our delayed solving of Auto plays into it. Idris will peek at LHS of CaseAlts to guess the type if it doesn't have one.
 - [ ] Can't skip an auto. We need `{{_}}` to be auto or `%search` syntax.
 - [x] add filenames to FC
 - [x] maybe use backtick for javascript so we don't highlight strings as JS
diff --git a/aoc2023/Day1.newt b/aoc2023/Day1.newt
index 8ac2e12..ebb2313 100644
--- a/aoc2023/Day1.newt
+++ b/aoc2023/Day1.newt
@@ -6,11 +6,9 @@ import Node
 digits1 : List Char -> List Int
 digits1 Nil = Nil
 digits1 (c :: cs) = let x = ord c in
-  case x < 58 of
-    True => case 48 < x of
-      True => x - 48 :: digits1 cs
-      False => digits1 cs
-    False => digits1 cs
+  if 48 < x && x < 58
+    then x - 48 :: digits1 cs
+    else digits1 cs
 
 tail : {a : U} -> List a -> List a
 tail Nil = Nil
diff --git a/aoc2023/Day2.newt b/aoc2023/Day2.newt
index 2fda72e..068459f 100644
--- a/aoc2023/Day2.newt
+++ b/aoc2023/Day2.newt
@@ -43,43 +43,38 @@ parseDraw line =
 
 parseGame : String -> Either String Game
 parseGame line =
-  -- Need the Idris | sugar...
-  case split line ": " of
-    -- this is splitting on the Nil instead of the a
-    (a :: b :: Nil) => case split a " " of
-      ("Game" :: ns :: Nil) =>
-        let num = toInt ns in
-        case mapM {Either String} parseDraw $ split b "; " of
-          Right parts => Right $ MkGame num parts
-          Left err => Left err
-      _ => Left "No Game"
-    _ => Left $ "No colon in " ++ line
+  let (a :: b :: Nil) = split line ": "
+    | _ => Left $ "No colon in " ++ line in
+  let ("Game" :: ns :: Nil) = split a " "
+    | _ => Left $ "No Game" in
+  let (Right parts) = mapM {Either String} parseDraw $ split b "; "
+    | Left err => Left err in
+  Right $ MkGame (toInt ns) parts
 
 part1 : List Game -> Int
 part1 Nil = 0
 part1 (MkGame n parts :: rest) =
   let total = foldl maxd (0,0,0) parts in
-  case lte total (12,13,14) of
-    True => n + part1 rest
-    False => part1 rest
+  if lte total (12,13,14)
+    then n + part1 rest
+    else part1 rest
 
 part2 : List Game -> Int
 part2 Nil = 0
 part2 (MkGame n parts :: rest) =
-  case foldl maxd (0,0,0) parts of
-    (a,b,c) => a * b * c + part2 rest
+  let (a,b,c) = foldl maxd (0,0,0) parts
+   in a * b * c + part2 rest
 
 run : String -> IO Unit
 run fn = do
   putStrLn fn
   text <- readFile fn
-  case mapM {Either String} parseGame (split (trim text) "\n") of
-    Left err => putStrLn $ "fail " ++ err
-    Right games => do
-      putStrLn "part1"
-      printLn (part1 games)
-      putStrLn "part2"
-      printLn (part2 games)
+  let (Right games) = mapM {Either String} parseGame (split (trim text) "\n")
+    | Left err => putStrLn $ "fail " ++ err
+  putStrLn "part1"
+  printLn (part1 games)
+  putStrLn "part2"
+  printLn (part2 games)
 
 main : IO Unit
 main = do
diff --git a/aoc2023/Day4.newt b/aoc2023/Day4.newt
index 534a8d7..39fb721 100644
--- a/aoc2023/Day4.newt
+++ b/aoc2023/Day4.newt
@@ -8,11 +8,9 @@ Round = List Int × List Int
 
 parseRound : String → Maybe Round
 parseRound s =
-  case split s ": " of
-    (a :: b :: Nil) => case split b " | " of
-      (l :: r :: Nil) => Just (nums l, nums r)
-      _ => Nothing
-    _ => Nothing
+  let (a :: b :: Nil) = split s ": "   | _ => Nothing in
+  let (l :: r :: Nil) = split b " | "  | _ => Nothing in
+  Just (nums l, nums r)
   where
     -- Nat or Int here?
     nums : String → List Int
@@ -50,14 +48,12 @@ run : String -> IO Unit
 run fn = do
   putStrLn fn
   text <- readFile fn
-
-  case parse text of
-    Nothing => putStrLn "fail"
-    Just cards => do
-      putStrLn "part1"
-      printLn (part1 cards)
-      putStrLn "part2"
-      printLn (part2 cards)
+  let (Just cards) = parse text
+    | _ => putStrLn "fail"
+  putStrLn "part1"
+  printLn (part1 cards)
+  putStrLn "part2"
+  printLn (part2 cards)
 
 -- 13/30
 -- 25004/14427616
diff --git a/aoc2023/Day5.newt b/aoc2023/Day5.newt
index 5cbeb46..3df60a7 100644
--- a/aoc2023/Day5.newt
+++ b/aoc2023/Day5.newt
@@ -33,14 +33,14 @@ parseFile : String → Either String Problem
 parseFile content = do
   let parts = split (trim content) "\n\n"
   -- TODO deconstructing let
-  case parts of
-    (first :: rest) => case split first ": " of
-      (_ :: x :: Nil) => do
-        let seeds = nums x
-        maps <- mapA (λ part => parseMap (split part "\n")) rest
-        Right $ MkProb seeds maps
-      _ => Left $ "expected ': ' in " ++ first
-    _ => Left $ "expected some parts"
+  let (first :: rest) = parts
+    | _ => Left "expected some parts"
+  let (_ :: x :: Nil) = split first ": "
+    | _ => Left $ "expected ': ' in " ++ first
+
+  let seeds = nums x
+  maps <- mapA (λ part => parseMap (split part "\n")) rest
+  Right $ MkProb seeds maps
 
 applyEntry : Int → MapEntry → Int
 applyEntry n (MkEntry dest src len) =
@@ -96,26 +96,23 @@ mkRanges Nil = Just Nil
 mkRanges _ = Nothing
 
 part2 : Problem → IO Unit
-part2 (MkProb seeds maps) =
-  case mkRanges seeds of
-    Nothing => printLn "odd seeds!"
-    Just ranges => do
-      let results = foldl apply ranges maps
-      -- putStrLn $ debugStr results
-      let answer = foldl min 99999999 $ map fst results
-      putStrLn $ "part2 " ++ show answer
+part2 (MkProb seeds maps) = do
+  let (Just ranges) = mkRanges seeds
+    | Nothing => printLn "odd seeds!"
+  let results = foldl apply ranges maps
+  -- putStrLn $ debugStr results
+  let answer = foldl min 99999999 $ map fst results
+  putStrLn $ "part2 " ++ show answer
 
 run : String -> IO Unit
 run fn = do
   putStrLn fn
   text <- readFile fn
-  case parseFile text of
-    Left err => putStrLn err
-    Right prob => do
-      putStrLn $ debugStr prob
-      part1 prob
-      -- putStrLn "part2"
-      part2 prob
+  let (Right prob) = parseFile text
+    | Left err => putStrLn err
+  putStrLn $ debugStr prob
+  part1 prob
+  part2 prob
 
 -- 35 / 46
 -- 282277027 / 11554135
diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr
index befcfbf..3165924 100644
--- a/src/Lib/Elab.idr
+++ b/src/Lib/Elab.idr
@@ -901,7 +901,18 @@ undo ((DoExpr fc tm) :: Nil) = pure tm
 undo ((DoExpr fc tm) :: xs) = pure $ RApp fc (RApp fc (RVar fc "_>>=_") tm Explicit) (RLam fc (BI fc "_" Explicit Many) !(undo xs)) Explicit
 -- undo ((DoExpr fc tm) :: xs) = pure $ RApp fc (RApp fc (RVar fc "_>>_") tm Explicit) !(undo xs) Explicit
 undo ((DoLet fc nm tm) :: xs) = RLet fc nm (RImplicit fc) tm <$> undo xs
-undo ((DoArrow fc nm tm) :: xs) = pure $ RApp fc (RApp fc (RVar fc "_>>=_") tm Explicit) (RLam fc (BI fc nm Explicit Many) !(undo xs)) Explicit
+undo ((DoArrow fc (RVar fc' nm) right []) :: xs) =
+  case lookup nm !get of
+    Just _ => ?todo
+    Nothing =>
+      pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit)
+        (RLam fc (BI fc' nm Explicit Many) !(undo xs)) Explicit
+
+undo ((DoArrow fc left right alts) :: xs) = do
+  let nm = "$sc"
+  rest <- pure $ RCase fc (RVar fc nm) (MkAlt left !(undo xs) :: alts)
+  pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit)
+    (RLam fc (BI fc nm Explicit Many) rest) Explicit
 
 check ctx tm ty = case (tm, !(forceType ctx.env ty)) of
   (RWhere fc decls body, ty) => checkWhere ctx (collectDecl decls) body ty
diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr
index ac51cc8..23fec96 100644
--- a/src/Lib/Parser.idr
+++ b/src/Lib/Parser.idr
@@ -154,6 +154,9 @@ parseOp = do
     | _ => fail "extra stuff"
   pure res
 
+
+
+
 export
 letExpr : Parser Raw
 letExpr = do
@@ -232,13 +235,54 @@ caseExpr = do
   alts <- startBlock $ someSame $ caseAlt
   pure $ RCase fc sc alts
 
-doStmt : Parser DoStmt
-doStmt
-  = DoArrow <$> getPos <*> (try $ ident <* keyword "<-") <*> term
-  <|> DoLet <$> getPos <* keyword "let" <*> ident <* keyword "=" <*> term
-  <|> DoExpr <$> getPos <*> term
-
 doExpr : Parser Raw
+doStmt : Parser DoStmt
+
+caseLet : Parser Raw
+caseLet = do
+  -- look ahead so we can fall back to normal let
+  fc <- getPos
+  try (keyword "let" >> sym "(")
+  pat <- typeExpr
+  sym ")"
+  keyword "="
+  sc <- typeExpr
+  alts <- startBlock $ manySame $ sym "|" *> caseAlt
+  keyword "in"
+  body <- term
+  pure $ RCase fc sc (MkAlt pat body :: alts)
+
+doCaseLet : Parser DoStmt
+doCaseLet = do
+  -- look ahead so we can fall back to normal let
+  -- Maybe make it work like arrow?
+  fc <- getPos
+  try (keyword "let" >> sym "(")
+  pat <- typeExpr
+  sym ")"
+  keyword "="
+  -- arrow <- (False <$ keyword "=" <|> True <$ keyword "<-")
+  sc <- typeExpr
+  alts <- startBlock $ manySame $ sym "|" *> caseAlt
+  bodyFC <- getPos
+  body <- RDo <$> getPos <*> someSame doStmt
+  pure $ DoExpr fc (RCase fc sc (MkAlt pat body :: alts))
+
+doArrow : Parser DoStmt
+doArrow = do
+  fc <- getPos
+  left <- typeExpr
+  Just _ <- optional $ keyword "<-"
+    | _ => pure $ DoExpr fc left
+  right <- term
+  alts <- startBlock $ manySame $ sym "|" *> caseAlt
+  pure $ DoArrow fc left right alts
+
+doStmt
+  = doCaseLet
+  <|> DoLet <$> getPos <* keyword "let" <*> ident <* keyword "=" <*> term
+  <|> doArrow
+
 doExpr = RDo <$> getPos <* keyword "do" <*> (startBlock $ someSame doStmt)
 
 ifThenElse : Parser Raw
@@ -254,6 +298,7 @@ ifThenElse = do
 
 -- This hits an idris codegen bug if parseOp is last and Lazy
 term =  caseExpr
+    <|> caseLet
     <|> letExpr
     <|> lamExpr
     <|> doExpr
diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr
index 10900b2..e67ac55 100644
--- a/src/Lib/Syntax.idr
+++ b/src/Lib/Syntax.idr
@@ -60,8 +60,7 @@ public export
 data DoStmt : Type where
   DoExpr : (fc : FC) -> Raw -> DoStmt
   DoLet : (fc : FC) -> String -> Raw -> DoStmt
-  DoArrow : (fc: FC) -> String -> Raw -> DoStmt
-
+  DoArrow : (fc: FC) -> Raw -> Raw -> List RCaseAlt -> DoStmt
 
 data Decl : Type
 data Raw : Type where
diff --git a/src/Lib/Tokenizer.idr b/src/Lib/Tokenizer.idr
index 2c942fc..d9d88d3 100644
--- a/src/Lib/Tokenizer.idr
+++ b/src/Lib/Tokenizer.idr
@@ -11,7 +11,7 @@ keywords = ["let", "in", "where", "case", "of", "data", "U", "do",
             "∀", "forall",
             "class", "instance",
             "if", "then", "else",
-             "->", "→", ":", "=>", ":=", "=", "<-", "\\", "_"]
+             "->", "→", ":", "=>", ":=", "=", "<-", "\\", "_", "|"]
 
 checkKW : String -> Token Kind
 checkKW s =