diff --git a/src/TTImp/Elab/Binders.idr b/src/TTImp/Elab/Binders.idr
index a3865e7..f2c19f5 100644
--- a/src/TTImp/Elab/Binders.idr
+++ b/src/TTImp/Elab/Binders.idr
@@ -109,3 +109,18 @@ checkLambda rig_in elabinfo env fc rigl info n argTy scope (Just expty_in)
                              (Just (gnf env
                                        (Bind fc bn (Pi rigb info pty) psc)))
               _ => inferLambda rig elabinfo env fc rigl info n argTy scope (Just expty_in)
+
+export
+checkLet : {vars : _} ->
+            {auto c : Ref Ctxt Defs} ->
+            {auto u : Ref UST UState} ->
+            {auto e : Ref EST (EState vars)} ->
+            RigCount -> ElabInfo -> Env Term vars -> 
+            FC -> 
+            RigCount -> (n : Name) -> 
+            (nTy : RawImp) -> (nVal : RawImp) -> (scope : RawImp) ->
+            (expTy : Maybe (Glued vars)) ->
+            Core (Term vars, Glued vars)
+checkLet rig_in elabinfo env fc rigl n nTy nVal scope expty
+    = throw (InternalError "let not implemented")
+
diff --git a/src/TTImp/Elab/Term.idr b/src/TTImp/Elab/Term.idr
index 6e2eb6e..a7bd86e 100644
--- a/src/TTImp/Elab/Term.idr
+++ b/src/TTImp/Elab/Term.idr
@@ -90,6 +90,14 @@ checkTerm rig elabinfo env (ILam fc r p (Just n) argTy scope) exp
 checkTerm rig elabinfo env (ILam fc r p Nothing argTy scope) exp 
     = do n <- genVarName "lam"
          checkLambda rig elabinfo env fc r p n argTy scope exp
+checkTerm rig elabinfo env (ILet fc r n nTy nVal scope) exp
+    = checkLet rig elabinfo env fc r n nTy nVal scope exp
+checkTerm rig elabinfo env (ICase fc scr scrty als) exp
+    = throw (InternalError "case not implemented")
+checkTerm rig elabinfo env (ILocal fc nested scope) exp
+    = throw (InternalError "let functions not implemented")
+checkTerm rig elabinfo env (IUpdate fc upds rec) exp
+    = throw (InternalError "record update not implemented")
 checkTerm rig elabinfo env (IApp fc fn arg) exp 
     = checkApp rig elabinfo env fc fn [arg] [] exp
 checkTerm rig elabinfo env (IImplicitApp fc fn nm arg) exp
@@ -107,14 +115,20 @@ checkTerm rig elabinfo env (ISearch fc depth) Nothing
          nm <- genName "search"
          sval <- searchVar fc rig depth (defining est) env nm ty
          pure (sval, gnf env ty)
+checkTerm rig elabinfo env (IAlternative fc atype alts) exp
+    = throw (InternalError "alternatives not implemented")
+checkTerm rig elabinfo env (IRewrite fc rule tm) exp
+    = throw (InternalError "rewrite not implemented")
+checkTerm rig elabinfo env (ICoerced fc tm) exp
+    = checkTerm rig elabinfo env tm exp
 checkTerm rig elabinfo env (IBindHere fc binder sc) exp
     = checkBindHere rig elabinfo env fc binder sc exp
 checkTerm rig elabinfo env (IBindVar fc n) exp
     = checkBindVar rig elabinfo env fc n exp
 checkTerm rig elabinfo env (IAs fc n tm) exp
-    = throw (InternalError "Not implemented")
+    = throw (InternalError "As patterns not implemented")
 checkTerm rig elabinfo env (IMustUnify fc n tm) exp
-    = throw (InternalError "Not implemented")
+    = throw (InternalError "Dot patterns implemented")
 
 checkTerm {vars} rig elabinfo env (IPrimVal fc c) exp 
     = do let (cval, cty) = checkPrim {vars} fc c
@@ -122,6 +136,8 @@ checkTerm {vars} rig elabinfo env (IPrimVal fc c) exp
 checkTerm rig elabinfo env (IType fc) exp 
     = checkExp rig elabinfo env fc (TType fc) (gType fc) exp
 
+checkTerm rig elabinfo env (IHole fc str) exp
+    = throw (InternalError "holes not implemented")
 checkTerm rig elabinfo env (Implicit fc b) (Just gexpty)
     = do nm <- genName "imp"
          expty <- getTerm gexpty
@@ -144,6 +160,24 @@ checkTerm rig elabinfo env (Implicit fc b) Nothing
          pure (metaval, gnf env ty)
 
 -- Declared in TTImp.Elab.Check
+-- check : {vars : _} ->
+--         {auto c : Ref Ctxt Defs} ->
+--         {auto u : Ref UST UState} ->
+--         {auto e : Ref EST (EState vars)} ->
+--         RigCount -> ElabInfo -> Env Term vars -> RawImp -> 
+--         Maybe (Glued vars) ->
+--         Core (Term vars, Glued vars)
+-- If we've just inserted an implicit coercion (in practice, that's either
+-- a force or delay) then check the term with any further insertions
+TTImp.Elab.Check.check rigc elabinfo env (ICoerced fc tm) exp
+    = checkImp rigc elabinfo env tm exp
+-- Don't add implicits/coercions on local blocks or record updates
+TTImp.Elab.Check.check rigc elabinfo env tm@(ILet fc c n nty nval sc) exp
+    = checkImp rigc elabinfo env tm exp
+TTImp.Elab.Check.check rigc elabinfo env tm@(ILocal fc ds sc) exp
+    = checkImp rigc elabinfo env tm exp
+TTImp.Elab.Check.check rigc elabinfo env tm@(IUpdate fc fs rec) exp
+    = checkImp rigc elabinfo env tm exp
 TTImp.Elab.Check.check rigc elabinfo env tm exp 
     = do defs <- get Ctxt
          case elabMode elabinfo of
@@ -152,6 +186,13 @@ TTImp.Elab.Check.check rigc elabinfo env tm exp
               _ => do tm' <- insertImpLam env tm exp
                       checkImp rigc elabinfo env tm' exp
 
+-- As above, but doesn't add any implicit lambdas, forces, delays, etc
+-- checkImp : {vars : _} ->
+--            {auto c : Ref Ctxt Defs} ->
+--            {auto u : Ref UST UState} ->
+--            {auto e : Ref EST (EState vars)} ->
+--            RigCount -> ElabInfo -> Env Term vars -> RawImp -> Maybe (Glued vars) ->
+--            Core (Term vars, Glued vars)
 TTImp.Elab.Check.checkImp rigc elabinfo env tm exp
     = checkTerm rigc elabinfo env tm exp
 
diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr
index 0f9df9b..e04f701 100644
--- a/src/TTImp/TTImp.idr
+++ b/src/TTImp/TTImp.idr
@@ -4,6 +4,8 @@ import Core.Context
 import Core.Env
 import Core.TT
 
+%default covering
+
 mutual
   public export
   data BindMode = PI RigCount | PATTERN | NONE
@@ -15,9 +17,20 @@ mutual
              (argTy : RawImp) -> (retTy : RawImp) -> RawImp
        ILam : FC -> RigCount -> PiInfo -> Maybe Name ->
               (argTy : RawImp) -> (lamTy : RawImp) -> RawImp
+       ILet : FC -> RigCount -> Name -> 
+              (nTy : RawImp) -> (nVal : RawImp) -> 
+              (scope : RawImp) -> RawImp 
+       ICase : FC -> RawImp -> (ty : RawImp) ->
+               List ImpClause -> RawImp
+       ILocal : FC -> List ImpDecl -> RawImp -> RawImp
+       IUpdate : FC -> List IFieldUpdate -> RawImp -> RawImp
+
        IApp : FC -> RawImp -> RawImp -> RawImp
        IImplicitApp : FC -> RawImp -> Maybe Name -> RawImp -> RawImp
        ISearch : FC -> (depth : Nat) -> RawImp
+       IAlternative : FC -> AltType -> List RawImp -> RawImp
+       IRewrite : FC -> RawImp -> RawImp -> RawImp
+       ICoerced : FC -> RawImp -> RawImp 
 
        -- Any implicit bindings in the scope should be bound here, using
        -- the given binder
@@ -31,6 +44,7 @@ mutual
        IMustUnify : FC -> (reason : String) -> RawImp -> RawImp
 
        IPrimVal : FC -> (c : Constant) -> RawImp
+       IHole : FC -> String -> RawImp
        IType : FC -> RawImp
 
        -- An implicit value, solved by unification, but which will also be
@@ -38,6 +52,17 @@ mutual
        -- at the end of elaborator                                                                     
        Implicit : FC -> (bindIfUnsolved : Bool) -> RawImp
 
+  public export
+  data IFieldUpdate : Type where
+       ISetField : (path : List String) -> RawImp -> IFieldUpdate
+       ISetFieldApp : (path : List String) -> RawImp -> IFieldUpdate
+
+  public export
+  data AltType : Type where
+       FirstSuccess : AltType
+       Unique : AltType
+       UniqueDefault : RawImp -> AltType
+
   export
     Show RawImp where
       show (IVar fc n) = show n
@@ -47,22 +72,44 @@ mutual
       show (ILam fc c p n arg sc)
          = "(%lam " ++ show c ++ " " ++ show p ++
            " " ++ show n ++ " " ++ show arg ++ " " ++ show sc ++ ")"
+      show (ILet fc c n ty val sc)
+         = "(%let " ++ show c ++ " " ++ " " ++ show n ++ " " ++ show ty ++ 
+           " " ++ show val ++ " " ++ show sc ++ ")"
+      show (ICase _ scr scrty alts)
+         = "(%case (" ++ show scr ++ ") " ++ show alts ++ ")"
+      show (ILocal _ def scope)
+         = "(%local (" ++ show def ++ ") " ++ show scope ++ ")"
+      show (IUpdate _ flds rec)
+         = "(%record " ++ showSep ", " (map show flds) ++ " " ++ show rec ++ ")"
+
       show (IApp fc f a)
          = "(" ++ show f ++ " " ++ show a ++ ")"
       show (IImplicitApp fc f n a)
          = "(" ++ show f ++ " [" ++ show n ++ " = " ++ show a ++ "])"
       show (ISearch fc d)
          = "%search"
+      show (IAlternative fc ty alts)
+         = "(|" ++ showSep "," (map show alts) ++ "|)"
+      show (IRewrite _ rule tm)
+         = "(%rewrite (" ++ show rule ++ ") (" ++ show tm ++ "))"
+      show (ICoerced _ tm) = show tm
+
       show (IBindHere fc b sc)
          = "(%bindhere " ++ show sc ++ ")"
       show (IBindVar fc n) = "$" ++ n
       show (IAs fc n tm) = show n ++ "@(" ++ show tm ++ ")"
       show (IMustUnify fc r tm) = ".(" ++ show tm ++ ")"
       show (IPrimVal fc c) = show c
+      show (IHole _ x) = "?" ++ x
       show (IType fc) = "%type"
       show (Implicit fc True) = "_"
       show (Implicit fc False) = "?"
 
+  export
+  Show IFieldUpdate where
+    show (ISetField p val) = showSep "->" p ++ " = " ++ show val
+    show (ISetFieldApp p val) = showSep "->" p ++ " $= " ++ show val
+
   public export
   data FnOpt : Type where
        Inline : FnOpt
@@ -135,6 +182,11 @@ mutual
     show (IClaim _ _ _ _ ty) = show ty
     show (IData _ _ d) = show d
     show (IDef _ n cs) = "(%def " ++ show n ++ " " ++ show cs ++ ")"
+    show (INamespace _ ns decls) 
+        = "namespace " ++ show ns ++ 
+          showSep "\n" (assert_total $ map show decls)
+    show (IPragma _) = "[externally defined pragma]"
+    show (ILog lvl) = "%logging " ++ show lvl
 
 -- REPL commands for TTImp interaction
 public export