From b1699ce0226bf576ee2617b61fa0802ad28aad04 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 4 Dec 2023 22:47:52 +0100
Subject: [PATCH] add let to the core

---
 lib/Quox/Displace.idr            |   2 +
 lib/Quox/FreeVars.idr            |  82 +++++++--------
 lib/Quox/Parser/FromParser.idr   |   5 +-
 lib/Quox/Pretty.idr              |   6 +-
 lib/Quox/Syntax/Term/Base.idr    |   5 +
 lib/Quox/Syntax/Term/Pretty.idr  |  46 +++++++++
 lib/Quox/Syntax/Term/Subst.idr   | 171 ++++++++++++++++---------------
 lib/Quox/Syntax/Term/Tighten.idr |   8 +-
 lib/Quox/Typechecker.idr         |  12 +++
 lib/Quox/Untyped/Erase.idr       |  19 ++++
 lib/Quox/Untyped/Syntax.idr      |   5 -
 lib/Quox/Whnf/Interface.idr      |   4 +
 lib/Quox/Whnf/Main.idr           |   5 +-
 13 files changed, 234 insertions(+), 136 deletions(-)

diff --git a/lib/Quox/Displace.idr b/lib/Quox/Displace.idr
index 3ac9907..6f8e1ed 100644
--- a/lib/Quox/Displace.idr
+++ b/lib/Quox/Displace.idr
@@ -34,6 +34,8 @@ parameters (k : Universe)
     doDisplace (Str s loc) = Str s loc
     doDisplace (BOX qty ty loc) = BOX qty (doDisplace ty) loc
     doDisplace (Box val loc) = Box (doDisplace val) loc
+    doDisplace (Let qty rhs body loc) =
+      Let qty (doDisplace rhs) (doDisplaceS body) loc
     doDisplace (E e) = E (doDisplace e)
     doDisplace (CloT (Sub t th)) =
       CloT (Sub (doDisplace t) (assert_total $ map doDisplace th))
diff --git a/lib/Quox/FreeVars.idr b/lib/Quox/FreeVars.idr
index 00ff22d..29c08ca 100644
--- a/lib/Quox/FreeVars.idr
+++ b/lib/Quox/FreeVars.idr
@@ -180,26 +180,27 @@ export HasFreeVars (Elim d)
 
 export
 HasFreeVars (Term d) where
-  fv (TYPE    {})            = none
-  fv (IOState {})            = none
-  fv (Pi      {arg, res, _}) = fv arg <+> fv res
-  fv (Lam     {body, _})     = fv body
-  fv (Sig     {fst, snd, _}) = fv fst <+> fv snd
-  fv (Pair    {fst, snd, _}) = fv fst <+> fv snd
-  fv (Enum    {})            = none
-  fv (Tag     {})            = none
-  fv (Eq      {ty, l, r, _}) = fvD ty <+> fv l <+> fv r
-  fv (DLam    {body, _})     = fvD body
-  fv (NAT     {})            = none
-  fv (Nat     {})            = none
-  fv (Succ    {p, _})        = fv p
-  fv (STRING  {})            = none
-  fv (Str     {})            = none
-  fv (BOX     {ty, _})       = fv ty
-  fv (Box     {val, _})      = fv val
-  fv (E       e)             = fv e
-  fv (CloT    s)             = fv s
-  fv (DCloT   s)             = fv s.term
+  fv (TYPE    {})             = none
+  fv (IOState {})             = none
+  fv (Pi      {arg, res, _})  = fv arg <+> fv res
+  fv (Lam     {body, _})      = fv body
+  fv (Sig     {fst, snd, _})  = fv fst <+> fv snd
+  fv (Pair    {fst, snd, _})  = fv fst <+> fv snd
+  fv (Enum    {})             = none
+  fv (Tag     {})             = none
+  fv (Eq      {ty, l, r, _})  = fvD ty <+> fv l <+> fv r
+  fv (DLam    {body, _})      = fvD body
+  fv (NAT     {})             = none
+  fv (Nat     {})             = none
+  fv (Succ    {p, _})         = fv p
+  fv (STRING  {})             = none
+  fv (Str     {})             = none
+  fv (BOX     {ty, _})        = fv ty
+  fv (Box     {val, _})       = fv val
+  fv (Let     {rhs, body, _}) = fv rhs <+> fv body
+  fv (E       e)              = fv e
+  fv (CloT    s)              = fv s
+  fv (DCloT   s)              = fv s.term
 
 export
 HasFreeVars (Elim d) where
@@ -258,26 +259,27 @@ export HasFreeDVars Elim
 
 export
 HasFreeDVars Term where
-  fdv (TYPE    {})            = none
-  fdv (IOState {})            = none
-  fdv (Pi      {arg, res, _}) = fdv arg <+> fdvT res
-  fdv (Lam     {body, _})     = fdvT body
-  fdv (Sig     {fst, snd, _}) = fdv fst <+> fdvT snd
-  fdv (Pair    {fst, snd, _}) = fdv fst <+> fdv snd
-  fdv (Enum    {})            = none
-  fdv (Tag     {})            = none
-  fdv (Eq      {ty, l, r, _}) = fdv @{DScope} ty <+> fdv l <+> fdv r
-  fdv (DLam    {body, _})     = fdv @{DScope} body
-  fdv (NAT     {})            = none
-  fdv (Nat     {})            = none
-  fdv (Succ    {p, _})        = fdv p
-  fdv (STRING  {})            = none
-  fdv (Str     {})            = none
-  fdv (BOX     {ty, _})       = fdv ty
-  fdv (Box     {val, _})      = fdv val
-  fdv (E       e)             = fdv e
-  fdv (CloT    s)             = fdv s @{WithSubst}
-  fdv (DCloT   s)             = fdvSubst s
+  fdv (TYPE    {})             = none
+  fdv (IOState {})             = none
+  fdv (Pi      {arg, res, _})  = fdv arg <+> fdvT res
+  fdv (Lam     {body, _})      = fdvT body
+  fdv (Sig     {fst, snd, _})  = fdv fst <+> fdvT snd
+  fdv (Pair    {fst, snd, _})  = fdv fst <+> fdv snd
+  fdv (Enum    {})             = none
+  fdv (Tag     {})             = none
+  fdv (Eq      {ty, l, r, _})  = fdv @{DScope} ty <+> fdv l <+> fdv r
+  fdv (DLam    {body, _})      = fdv @{DScope} body
+  fdv (NAT     {})             = none
+  fdv (Nat     {})             = none
+  fdv (Succ    {p, _})         = fdv p
+  fdv (STRING  {})             = none
+  fdv (Str     {})             = none
+  fdv (BOX     {ty, _})        = fdv ty
+  fdv (Box     {val, _})       = fdv val
+  fdv (Let     {rhs, body, _}) = fdv rhs <+> fdvT body
+  fdv (E       e)              = fdv e
+  fdv (CloT    s)              = fdv s @{WithSubst}
+  fdv (DCloT   s)              = fdvSubst s
 
 export
 HasFreeDVars Elim where
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index 75c2bdf..b252f73 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -265,7 +265,10 @@ mutual
         <*> pure loc
 
     Let (qty, x, rhs) body loc =>
-      ?fromPTerm_let
+      Let (fromPQty qty)
+        <$> fromPTermElim ds ns rhs
+        <*> fromPTermTScope ds ns [< x] body
+        <*> pure loc
 
   private
   fromPTermEnumArms : Loc -> Context' PatVar d -> Context' PatVar n ->
diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr
index 11aab94..3472479 100644
--- a/lib/Quox/Pretty.idr
+++ b/lib/Quox/Pretty.idr
@@ -267,8 +267,8 @@ prettyDBind = hl DVar . prettyBind'
 
 export %inline
 typeD, ioStateD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD,
-stringD, eqD, colonD, commaD, semiD, atD, caseD, typecaseD, returnD,
-ofD, dotD, zeroD, succD, coeD, compD, undD, cstD, pipeD, fstD, sndD :
+stringD, eqD, colonD, commaD, semiD, atD, caseD, typecaseD, returnD, ofD, dotD,
+zeroD, succD, coeD, compD, undD, cstD, pipeD, fstD, sndD, letD, inD :
   {opts : LayoutOpts} -> Eff Pretty (Doc opts)
 typeD     = hl Syntax . text =<< ifUnicode "★" "Type"
 ioStateD  = hl Syntax $ text "IOState"
@@ -300,6 +300,8 @@ cstD      = hl Syntax   $ text "="
 pipeD     = hl Delim    $ text "|"
 fstD      = hl Syntax   $ text "fst"
 sndD      = hl Syntax   $ text "snd"
+letD      = hl Syntax   $ text "let"
+inD       = hl Syntax   $ text "in"
 
 
 export
diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index 994b4ea..36715d4 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -99,6 +99,9 @@ mutual
     BOX : (qty : Qty) -> (ty : Term d n) -> (loc : Loc) -> Term d n
     Box : (val : Term d n) -> (loc : Loc) -> Term d n
 
+    Let : (qty : Qty) -> (rhs : Elim d n) ->
+          (body : ScopeTerm d n) -> (loc : Loc) -> Term d n
+
     ||| elimination
     E : (e : Elim d n) -> Term d n
 
@@ -383,6 +386,7 @@ Located (Term d n) where
   (Succ _ loc).loc      = loc
   (BOX _ _ loc).loc     = loc
   (Box _ loc).loc       = loc
+  (Let _ _ _ loc).loc   = loc
   (E e).loc             = e.loc
   (CloT (Sub t _)).loc  = t.loc
   (DCloT (Sub t _)).loc = t.loc
@@ -446,6 +450,7 @@ Relocatable (Term d n) where
   setLoc loc (Str s _) = Str s loc
   setLoc loc (BOX qty ty _) = BOX qty ty loc
   setLoc loc (Box val _) = Box val loc
+  setLoc loc (Let qty rhs body _) = Let qty rhs body loc
   setLoc loc (E e) = E $ setLoc loc e
   setLoc loc (CloT (Sub term subst)) = CloT $ Sub (setLoc loc term) subst
   setLoc loc (DCloT (Sub term subst)) = DCloT $ Sub (setLoc loc term) subst
diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index 7b9f89e..e686a74 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -317,6 +317,44 @@ prettyCase dnames tnames qty head ret body =
   prettyCase_ dnames tnames ![|caseD <+> prettyQty qty|] head ret body
 
 
+private
+LetBinder : Nat -> Nat -> Type
+LetBinder d n = (Qty, BindName, Elim d n)
+
+private
+LetExpr : Nat -> Nat -> Nat -> Type
+LetExpr d n n' = (Telescope (LetBinder d) n n', Term d n')
+
+private
+PrettyLetResult : LayoutOpts -> Nat -> Type
+PrettyLetResult opts d =
+  Exists $ \n => (BContext n, Term d n, SnocList (Doc opts))
+
+-- [todo] factor out this and the untyped version somehow
+export
+splitLet : Telescope (LetBinder d) n n' -> Term d n' -> Exists (LetExpr d n)
+splitLet ys t@(Let qty rhs body _) =
+  splitLet (ys :< (qty, body.name, rhs)) (assert_smaller t body.term)
+splitLet ys t =
+  Evidence _ (ys, t)
+
+private covering
+prettyLets : {opts : LayoutOpts} ->
+             BContext d -> BContext a -> Telescope (LetBinder d) a b ->
+             Eff Pretty (SnocList (Doc opts))
+prettyLets dnames xs lets = sequence $ snd $ go lets where
+  go : forall b. Telescope (LetBinder d) a b ->
+       (BContext b, SnocList (Eff Pretty (Doc opts)))
+  go [<] = (xs, [<])
+  go (lets :< (qty, x, rhs)) =
+    let (ys, docs) = go lets
+        doc = do
+          x   <- prettyTBind x
+          rhs <- withPrec Outer $ assert_total prettyElim dnames ys rhs
+          hangDSingle (hsep [!letD, x, !cstD]) (hsep [rhs, !inD]) in
+    (ys :< x, docs :< doc)
+
+
 private
 isDefaultDir : Dim d -> Dim d -> Bool
 isDefaultDir (K Zero _) (K One _) = True
@@ -457,6 +495,14 @@ prettyTerm dnames tnames (BOX qty ty _) =
 prettyTerm dnames tnames (Box val _) =
   bracks =<< withPrec Outer (prettyTerm dnames tnames val)
 
+prettyTerm dnames tnames (Let qty rhs body _) = do
+  let Evidence _ (lets, body) = splitLet [< (qty, body.name, rhs)] body.term
+  heads <- prettyLets dnames tnames lets
+  let tnames = tnames . map (\(_, x, _) => x) lets
+  body <- withPrec Outer $ assert_total prettyTerm dnames tnames body
+  let lines = toList $ heads :< body
+  pure $ ifMultiline (hsep lines) (vsep lines)
+
 prettyTerm dnames tnames (E e) = prettyElim dnames tnames e
 
 prettyTerm dnames tnames t0@(CloT (Sub t ph)) =
diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index b85ffd4..330a10e 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -249,89 +249,90 @@ mutual
   isCloE (DCloE {}) = True
   isCloE _          = False
 
-mutual
-  export
-  PushSubsts Term Subst.isCloT where
-    pushSubstsWith th ph (TYPE l loc) =
-      nclo $ TYPE l loc
-    pushSubstsWith th ph (IOState loc) =
-      nclo $ IOState loc
-    pushSubstsWith th ph (Pi qty a body loc) =
-      nclo $ Pi qty (a // th // ph) (body // th // ph) loc
-    pushSubstsWith th ph (Lam body loc) =
-      nclo $ Lam (body // th // ph) loc
-    pushSubstsWith th ph (Sig a b loc) =
-      nclo $ Sig (a // th // ph) (b // th // ph) loc
-    pushSubstsWith th ph (Pair s t loc) =
-      nclo $ Pair (s // th // ph) (t // th // ph) loc
-    pushSubstsWith th ph (Enum tags loc) =
-      nclo $ Enum tags loc
-    pushSubstsWith th ph (Tag tag loc) =
-      nclo $ Tag tag loc
-    pushSubstsWith th ph (Eq ty l r loc) =
-      nclo $ Eq (ty // th // ph) (l // th // ph) (r // th // ph) loc
-    pushSubstsWith th ph (DLam body loc) =
-      nclo $ DLam (body // th // ph) loc
-    pushSubstsWith _ _ (NAT loc) =
-      nclo $ NAT loc
-    pushSubstsWith _ _ (Nat n loc) =
-      nclo $ Nat n loc
-    pushSubstsWith th ph (Succ n loc) =
-      nclo $ Succ (n // th // ph) loc
-    pushSubstsWith _ _ (STRING loc) =
-      nclo $ STRING loc
-    pushSubstsWith _ _ (Str s loc) =
-      nclo $ Str s loc
-    pushSubstsWith th ph (BOX pi ty loc) =
-      nclo $ BOX pi (ty // th // ph) loc
-    pushSubstsWith th ph (Box val loc) =
-      nclo $ Box (val // th // ph) loc
-    pushSubstsWith th ph (E e) =
-      let Element e nc = pushSubstsWith th ph e in nclo $ E e
-    pushSubstsWith th ph (CloT (Sub s ps)) =
-      pushSubstsWith th (comp th ps ph) s
-    pushSubstsWith th ph (DCloT (Sub s ps)) =
-      pushSubstsWith (ps . th) ph s
+export
+PushSubsts Elim Subst.isCloE where
+  pushSubstsWith th ph (F x u loc) =
+    nclo $ F x u loc
+  pushSubstsWith th ph (B i loc) =
+    let res = getLoc ph i loc in
+    case nchoose $ isCloE res of
+      Left  yes => assert_total pushSubsts res
+      Right no  => Element res no
+  pushSubstsWith th ph (App f s loc) =
+    nclo $ App (f // th // ph) (s // th // ph) loc
+  pushSubstsWith th ph (CasePair pi p r b loc) =
+    nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph) loc
+  pushSubstsWith th ph (Fst pair loc) =
+    nclo $ Fst (pair // th // ph) loc
+  pushSubstsWith th ph (Snd pair loc) =
+    nclo $ Snd (pair // th // ph) loc
+  pushSubstsWith th ph (CaseEnum pi t r arms loc) =
+    nclo $ CaseEnum pi (t // th // ph) (r // th // ph)
+             (map (\b => b // th // ph) arms) loc
+  pushSubstsWith th ph (CaseNat pi pi' n r z s loc) =
+    nclo $ CaseNat pi pi' (n // th // ph) (r // th // ph)
+             (z // th // ph) (s // th // ph) loc
+  pushSubstsWith th ph (CaseBox pi x r b loc) =
+    nclo $ CaseBox pi (x // th // ph) (r // th // ph) (b // th // ph) loc
+  pushSubstsWith th ph (DApp f d loc) =
+    nclo $ DApp (f // th // ph) (d // th) loc
+  pushSubstsWith th ph (Ann s a loc) =
+    nclo $ Ann (s // th // ph) (a // th // ph) loc
+  pushSubstsWith th ph (Coe ty p q val loc) =
+    nclo $ Coe (ty // th // ph) (p // th) (q // th) (val // th // ph) loc
+  pushSubstsWith th ph (Comp ty p q val r zero one loc) =
+    nclo $ Comp (ty // th // ph) (p // th) (q // th)
+                (val // th // ph) (r // th)
+                (zero // th // ph) (one // th // ph) loc
+  pushSubstsWith th ph (TypeCase ty ret arms def loc) =
+    nclo $ TypeCase (ty // th // ph) (ret  // th // ph)
+      (map (\t => t // th // ph) arms) (def // th // ph) loc
+  pushSubstsWith th ph (CloE (Sub e ps)) =
+    pushSubstsWith th (comp th ps ph) e
+  pushSubstsWith th ph (DCloE (Sub e ps)) =
+    pushSubstsWith (ps . th) ph e
 
-  export
-  PushSubsts Elim Subst.isCloE where
-    pushSubstsWith th ph (F x u loc) =
-      nclo $ F x u loc
-    pushSubstsWith th ph (B i loc) =
-      let res = getLoc ph i loc in
-      case nchoose $ isCloE res of
-        Left  yes => assert_total pushSubsts res
-        Right no  => Element res no
-    pushSubstsWith th ph (App f s loc) =
-      nclo $ App (f // th // ph) (s // th // ph) loc
-    pushSubstsWith th ph (CasePair pi p r b loc) =
-      nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph) loc
-    pushSubstsWith th ph (Fst pair loc) =
-      nclo $ Fst (pair // th // ph) loc
-    pushSubstsWith th ph (Snd pair loc) =
-      nclo $ Snd (pair // th // ph) loc
-    pushSubstsWith th ph (CaseEnum pi t r arms loc) =
-      nclo $ CaseEnum pi (t // th // ph) (r // th // ph)
-               (map (\b => b // th // ph) arms) loc
-    pushSubstsWith th ph (CaseNat pi pi' n r z s loc) =
-      nclo $ CaseNat pi pi' (n // th // ph) (r // th // ph)
-               (z // th // ph) (s // th // ph) loc
-    pushSubstsWith th ph (CaseBox pi x r b loc) =
-      nclo $ CaseBox pi (x // th // ph) (r // th // ph) (b // th // ph) loc
-    pushSubstsWith th ph (DApp f d loc) =
-      nclo $ DApp (f // th // ph) (d // th) loc
-    pushSubstsWith th ph (Ann s a loc) =
-      nclo $ Ann (s // th // ph) (a // th // ph) loc
-    pushSubstsWith th ph (Coe ty p q val loc) =
-      nclo $ Coe (ty // th // ph) (p // th) (q // th) (val // th // ph) loc
-    pushSubstsWith th ph (Comp ty p q val r zero one loc) =
-      nclo $ Comp (ty // th // ph) (p // th) (q // th)
-                  (val // th // ph) (r // th)
-                  (zero // th // ph) (one // th // ph) loc
-    pushSubstsWith th ph (TypeCase ty ret arms def loc) =
-      nclo $ TypeCase (ty // th // ph) (ret  // th // ph)
-        (map (\t => t // th // ph) arms) (def // th // ph) loc
-    pushSubstsWith th ph (CloE (Sub e ps)) =
-      pushSubstsWith th (comp th ps ph) e
-    pushSubstsWith th ph (DCloE (Sub e ps)) =
-      pushSubstsWith (ps . th) ph e
+export
+PushSubsts Term Subst.isCloT where
+  pushSubstsWith th ph (TYPE l loc) =
+    nclo $ TYPE l loc
+  pushSubstsWith th ph (IOState loc) =
+    nclo $ IOState loc
+  pushSubstsWith th ph (Pi qty a body loc) =
+    nclo $ Pi qty (a // th // ph) (body // th // ph) loc
+  pushSubstsWith th ph (Lam body loc) =
+    nclo $ Lam (body // th // ph) loc
+  pushSubstsWith th ph (Sig a b loc) =
+    nclo $ Sig (a // th // ph) (b // th // ph) loc
+  pushSubstsWith th ph (Pair s t loc) =
+    nclo $ Pair (s // th // ph) (t // th // ph) loc
+  pushSubstsWith th ph (Enum tags loc) =
+    nclo $ Enum tags loc
+  pushSubstsWith th ph (Tag tag loc) =
+    nclo $ Tag tag loc
+  pushSubstsWith th ph (Eq ty l r loc) =
+    nclo $ Eq (ty // th // ph) (l // th // ph) (r // th // ph) loc
+  pushSubstsWith th ph (DLam body loc) =
+    nclo $ DLam (body // th // ph) loc
+  pushSubstsWith _ _ (NAT loc) =
+    nclo $ NAT loc
+  pushSubstsWith _ _ (Nat n loc) =
+    nclo $ Nat n loc
+  pushSubstsWith th ph (Succ n loc) =
+    nclo $ Succ (n // th // ph) loc
+  pushSubstsWith _ _ (STRING loc) =
+    nclo $ STRING loc
+  pushSubstsWith _ _ (Str s loc) =
+    nclo $ Str s loc
+  pushSubstsWith th ph (BOX pi ty loc) =
+    nclo $ BOX pi (ty // th // ph) loc
+  pushSubstsWith th ph (Box val loc) =
+    nclo $ Box (val // th // ph) loc
+  pushSubstsWith th ph (E e) =
+    let Element e nc = pushSubstsWith th ph e in nclo $ E e
+  pushSubstsWith th ph (Let qty rhs body loc) =
+    nclo $ Let qty (rhs // th // ph) (body // th // ph) loc
+  pushSubstsWith th ph (CloT (Sub s ps)) =
+    pushSubstsWith th (comp th ps ph) s
+  pushSubstsWith th ph (DCloT (Sub s ps)) =
+    pushSubstsWith (ps . th) ph s
diff --git a/lib/Quox/Syntax/Term/Tighten.idr b/lib/Quox/Syntax/Term/Tighten.idr
index de45d98..0709684 100644
--- a/lib/Quox/Syntax/Term/Tighten.idr
+++ b/lib/Quox/Syntax/Term/Tighten.idr
@@ -75,8 +75,10 @@ mutual
     BOX qty <$> tightenT p ty <*> pure loc
   tightenT' p (Box val loc) =
     Box <$> tightenT p val <*> pure loc
+  tightenT' p (Let qty rhs body loc) =
+    Let qty <$> assert_total tightenE p rhs <*> tightenS p body <*> pure loc
   tightenT' p (E e) =
-    assert_total $ E <$> tightenE p e
+    E <$> assert_total tightenE p e
 
   private
   tightenE' : OPE n1 n2 -> (e : Elim d n2) -> (0 ne : NotClo e) =>
@@ -200,8 +202,10 @@ mutual
     BOX qty <$> dtightenT p ty <*> pure loc
   dtightenT' p (Box val loc) =
     Box <$> dtightenT p val <*> pure loc
+  dtightenT' p (Let qty rhs body loc) =
+    Let qty <$> assert_total dtightenE p rhs <*> dtightenS p body <*> pure loc
   dtightenT' p (E e) =
-    assert_total $ E <$> dtightenE p e
+    E <$> assert_total dtightenE p e
 
   export
   dtightenE' : OPE d1 d2 -> (e : Elim d2 n) -> (0 ne : NotClo e) =>
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index a477c3e..13052b1 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -213,6 +213,13 @@ mutual
     -- then Ψ | Γ ⊢ σ · [s] ⇐ [π.A] ⊳ πΣ
     pure $ q * valout
 
+  check' ctx sg (Let qty rhs body loc) ty = do
+    eres <- inferC ctx (subjMult sg qty) rhs
+    qout <- checkC (extendTy (qty * sg.qty) body.name eres.type ctx) sg
+              body.term (weakT 1 ty)
+        >>= popQ loc qty
+    pure $ qty * eres.qout + qout
+
   check' ctx sg (E e) ty = do
     -- if Ψ | Γ ⊢ σ · e ⇒ A' ⊳ Σ
     infres <- inferC ctx sg e
@@ -286,6 +293,11 @@ mutual
   checkType' ctx (BOX q ty _) u = checkType ctx ty u
   checkType' ctx t@(Box {}) u = throw $ NotType t.loc ctx t
 
+  checkType' ctx (Let qty rhs body loc) u = do
+    expectEqualQ loc qty Zero
+    ety <- inferC ctx SZero rhs
+    checkType (extendTy Zero body.name ety.type ctx) body.term u
+
   checkType' ctx (E e) u = do
     -- if Ψ | Γ ⊢₀ E ⇒ Type ℓ
     infres <- inferC ctx SZero e
diff --git a/lib/Quox/Untyped/Erase.idr b/lib/Quox/Untyped/Erase.idr
index 0fc24ef..43630c2 100644
--- a/lib/Quox/Untyped/Erase.idr
+++ b/lib/Quox/Untyped/Erase.idr
@@ -222,6 +222,25 @@ eraseTerm ctx ty (Box val loc) = do
     Erased => pure $ Erased loc
     Kept   => eraseTerm ctx a val
 
+--         s ⤋ s' ⇐ A
+-- ----------------------------
+--   let0 x = e in s ⤋ s' ⇐ A
+--
+--     e ⤋ e'  s ⤋ s' ⇐ A   π ≠ 0
+-- -------------------------------------
+--  letπ x = e in s ⤋ let x = e' in s'
+eraseTerm ctx ty (Let pi e s loc) = do
+  let x = s.name
+  case isErased pi of
+    Erased => do
+      ety <- computeElimType ctx SZero e
+      s'  <- eraseTerm (extendTy pi x ety ctx) (weakT 1 ty) s.term
+      pure $ sub1 (Erased e.loc) s'
+    Kept => do
+      EraRes ety e' <- eraseElim ctx e
+      s' <- eraseTerm (extendTy pi x ety ctx) (weakT 1 ty) s.term
+      pure $ Let x e' s' loc
+
 --  e ⤋ e' ⇒ B
 -- ------------
 --  e ⤋ e' ⇐ A
diff --git a/lib/Quox/Untyped/Syntax.idr b/lib/Quox/Untyped/Syntax.idr
index da660cd..5df044d 100644
--- a/lib/Quox/Untyped/Syntax.idr
+++ b/lib/Quox/Untyped/Syntax.idr
@@ -96,11 +96,6 @@ public export
 Definitions = SortedMap Name Definition
 
 
-export
-letD, inD : {opts : LayoutOpts} -> Eff Pretty (Doc opts)
-letD = hl Syntax "let"
-inD  = hl Syntax "in"
-
 export covering
 prettyTerm : {opts : LayoutOpts} -> BContext n ->
              Term n -> Eff Pretty (Doc opts)
diff --git a/lib/Quox/Whnf/Interface.idr b/lib/Quox/Whnf/Interface.idr
index efc51f9..15a8978 100644
--- a/lib/Quox/Whnf/Interface.idr
+++ b/lib/Quox/Whnf/Interface.idr
@@ -135,6 +135,7 @@ isTyCon (STRING  {}) = True
 isTyCon (Str     {}) = False
 isTyCon (BOX     {}) = True
 isTyCon (Box     {}) = False
+isTyCon (Let     {}) = False
 isTyCon (E       {}) = False
 isTyCon (CloT    {}) = False
 isTyCon (DCloT   {}) = False
@@ -182,6 +183,7 @@ canPushCoe sg (STRING  {}) _         = True
 canPushCoe sg (Str     {}) _         = False
 canPushCoe sg (BOX     {}) _         = True
 canPushCoe sg (Box     {}) _         = False
+canPushCoe sg (Let     {}) _         = False
 canPushCoe sg (E       {}) _         = False
 canPushCoe sg (CloT    {}) _         = False
 canPushCoe sg (DCloT   {}) _         = False
@@ -243,10 +245,12 @@ mutual
   |||    (the annotation is redundant in a checkable context)
   ||| 3. a closure
   ||| 4. `succ` applied to a natural constant
+  ||| 5. a `let` expression
   public export
   isRedexT : RedexTest Term
   isRedexT _    _  (CloT  {})  = True
   isRedexT _    _  (DCloT {})  = True
+  isRedexT _    _  (Let   {})  = True
   isRedexT defs sg (E {e, _})  = isAnn e || isRedexE defs sg e
   isRedexT _    _  (Succ p {}) = isNatConst p
   isRedexT _    _  _           = False
diff --git a/lib/Quox/Whnf/Main.idr b/lib/Quox/Whnf/Main.idr
index e636adf..9248edf 100644
--- a/lib/Quox/Whnf/Main.idr
+++ b/lib/Quox/Whnf/Main.idr
@@ -252,7 +252,10 @@ CanWhnf Term Interface.isRedexT where
       Left _ => case p of
         Nat p _               => pure $ nred $ Nat (S p) loc
         E (Ann (Nat p _) _ _) => pure $ nred $ Nat (S p) loc
-      Right nc => pure $ Element (Succ p loc) $ ?cc
+      Right nc => pure $ Element (Succ p loc) nc
+
+  whnf defs ctx sg (Let _ rhs body _) =
+    whnf defs ctx sg $ sub1 body rhs
 
   -- s ∷ A ⇝ s   (in term context)
   whnf defs ctx sg (E e) = do