elaborate let

TODO.md

@@ -5,7 +5,7 @@ I may be done with `U` - I keep typing `Type`.
 
 - [x] switch from commit/mustWork to checking progress
 - [x] type constructors are no longer generated?  And seem to have 0 arity.
-- [ ] raw let is not yet implemented (although define used by case tree building)
+- [x] raw let is not yet implemented (although define used by case tree building)
 - [x] there is some zero argument application in generated code
 - [x] get equality.newt to work
   - [x] broken again because I added J, probably need to constrain scrutinee to value

src/Lib/Check.idr

@@ -650,7 +650,15 @@ infer ctx (RPi fc nm icit ty ty2) = do
   let nm := fromMaybe "_" nm
   ty2' <- check (extend ctx nm vty') ty2 (VU fc)
   pure (Pi fc nm icit ty' ty2', (VU fc))
-infer ctx (RLet fc nm ty v sc) = error fc "implement RLet"
+infer ctx (RLet fc nm ty v sc) = do
+  ty' <- check ctx ty (VU emptyFC)
+  vty <- eval ctx.env CBN ty'
+  v' <- check ctx v vty
+  vv <- eval ctx.env CBN v'
+  let ctx' = define ctx nm vv vty
+  (sc',scty) <- infer ctx' sc
+  pure $ (Let fc nm v' sc', scty)
+
 infer ctx (RAnn fc tm rty) = do
   ty <- check ctx rty (VU fc)
   vty <- eval ctx.env CBN ty

tests/black/let.newt

@@ -0,0 +1,6 @@
+module Let
+
+ptype Int
+
+foo : Int -> Int
+foo n = let x = 42 in x