diff --git a/src/Commands.newt b/src/Commands.newt
index 98d7c74..c768cf9 100644
--- a/src/Commands.newt
+++ b/src/Commands.newt
@@ -38,7 +38,7 @@ switchModule repo modns = do
     top <- getTop
     -- mod <- processModule emptyFC repo Nil modns
     let (Just mod) = lookupMap' modns top.modules | Nothing => pure Nothing
-    modifyTop [ currentMod := mod; ops := mod.modOps ]
+    modifyTop { currentMod := mod; ops := mod.modOps }
     pure $ Just mod
 
 data HoverInfo = NoHoverInfo | NeedCheck | HasHover FC String
diff --git a/src/LSP.newt b/src/LSP.newt
index a7fd4c9..47ef6b6 100644
--- a/src/LSP.newt
+++ b/src/LSP.newt
@@ -68,12 +68,12 @@ lspFileSource = do
 
 updateFile : String → String → Unit
 updateFile fn src = unsafePerformIO $ do
-    modifyIORef state [ files $= updateMap fn src ]
+    modifyIORef state { files $= updateMap fn src }
     st <- readIORef state
     let (base,modName) = decomposeName fn
     Right (ctx,_) <- (invalidateModule modName).runM st.topContext
         | _ => writeIORef state st
-    modifyIORef state [ topContext := ctx ]
+    modifyIORef state { topContext := ctx }
 
 
 fcToRange : FC → Json
@@ -96,17 +96,17 @@ hoverInfo uri line col = unsafePerformIO $ do
     -- We're proactively running check if there is no module information, make sure we save it
     Right (top, HasHover fc msg) <- (getHoverInfo repo modns line col).runM st.topContext
         | Right (top, NeedCheck)  => do
-            modifyIORef state $ [ topContext := top ]
+            modifyIORef state $ { topContext := top }
             putStrLn $ "NeedsCheck"
             pure $ js_castBool True
         | Right (top, NoHoverInfo)  => do
-            modifyIORef state $ [ topContext := top ]
+            modifyIORef state $ { topContext := top }
             putStrLn $ "Nothing to see here"
             pure $ js_castBool True
         | Left err => do
             putStrLn $ showError "" err
             pure $ jsonToJObject JsonNull
-    modifyIORef state $ [ topContext := top ]
+    modifyIORef state $ { topContext := top }
     let location = JsonObj $ ("uri", JsonStr fc.file) :: ("range", fcToRange fc) :: Nil
     pure $ jsonToJObject $ JsonObj $ ("info", JsonStr msg) :: ("location", location) :: Nil
 
@@ -126,7 +126,7 @@ codeActionInfo uri line col = unsafePerformIO $ do
       putStrLn "ACTIONS ERROR"
       putStrLn $ showError "" err
       pure js_null
-  modifyIORef state $ [ topContext := top ]
+  modifyIORef state $ { topContext := top }
   pure $ jsonToJObject $ JsonArray $ map actionToJson actions
   where
     single : String → Json → Json
@@ -238,7 +238,7 @@ checkFile fn = unsafePerformIO $ do
     (Right (top, json)) <- (do
         putStrLn "processModule"
         mod <- processModule emptyFC repo Nil modName
-        modifyTop [ currentMod := mod; ops := mod.modOps ]
+        modifyTop { currentMod := mod; ops := mod.modOps }
 
         -- pull out errors and infos
         top <- getTop
@@ -251,7 +251,7 @@ checkFile fn = unsafePerformIO $ do
             putStrLn $ showError "" err
             pure $ jsonToJObject $ JsonArray $ errorToDiag err :: Nil
     -- Cache loaded modules
-    modifyIORef state $ [ topContext := top ]
+    modifyIORef state $ { topContext := top }
     pure $ jsonToJObject $ JsonArray json
 
 docSymbols : String → JSObject
@@ -265,11 +265,11 @@ docSymbols fn = unsafePerformIO $ do
     repo <- lspFileSource
     (Right (top, json)) <- (do
         mod <- processModule emptyFC repo Nil modName
-        modifyTop [ currentMod := mod; ops := mod.modOps ]
+        modifyTop { currentMod := mod; ops := mod.modOps }
         getSymbols).runM st.topContext
         | Left err => do
            pure $ jsonToJObject $ JsonNull
-    modifyIORef state $ [ topContext := top ]
+    modifyIORef state $ { topContext := top }
     pure $ jsonToJObject $ JsonArray json
 
 compileJS : String → JSObject
@@ -287,7 +287,7 @@ compileJS fn = unsafePerformIO $ do
           ++ map (render 90 ∘ noAlt) docs
     pure src).runM st.topContext
     | Left err => pure $ js_castStr "// \{errorMsg err}"
-  modifyIORef state [ topContext := top ]
+  modifyIORef state { topContext := top }
   pure $ js_castStr src
 
 compileToScheme : String → JSObject
@@ -302,7 +302,7 @@ compileToScheme fn = unsafePerformIO $ do
     let src = unlines docs
     pure src).runM st.topContext
     | Left err => pure $ js_castStr ";; \{errorMsg err}"
-  modifyIORef state [ topContext := top ]
+  modifyIORef state { topContext := top }
   pure $ js_castStr src
 
 #export updateFile checkFile hoverInfo codeActionInfo compileJS docSymbols compileToScheme
diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt
index 16c45ef..2387280 100644
--- a/src/Lib/Elab.newt
+++ b/src/Lib/Elab.newt
@@ -118,10 +118,10 @@ isCandidate _ _ = False
 
 setMetaMode : MetaMode → M Unit
 -- ideally we would support dotted paths like metaCtx.mcmode := CheckFirst
-setMetaMode mcmode = modifyTop [ currentMod $= [modMetaCtx $= [mcmode := mcmode] ] ]
+setMetaMode mcmode = modifyTop { currentMod $= {modMetaCtx $= {mcmode := mcmode} } }
 
 setMetaContext : MetaContext → M Unit
-setMetaContext mc = modifyTop [ currentMod $= [ modMetaCtx := mc ]]
+setMetaContext mc = modifyTop { currentMod $= { modMetaCtx := mc }}
 
 findMatches : Context -> Val -> List (QName × Tm) -> M (List QName)
 findMatches ctx ty Nil = pure Nil
@@ -255,7 +255,7 @@ updateMeta ix f = do
   let autos = case me of
     Solved _ _ _ => filter (_/=_ ix) mc.autos
     _ => mc.autos
-  setMetaContext $ [metas $= updateMap ix me; autos := autos] mc
+  setMetaContext $ {metas $= updateMap ix me; autos := autos} mc
 
 -- Try to solve autos that reference the meta ix
 checkAutos : QName -> List QName -> M Unit
@@ -618,7 +618,7 @@ freshMeta ctx fc ty kind = do
   let autos = case kind of
       AutoSolve => qn :: mc.autos
       _ => mc.autos
-  setMetaContext $ [ metas $= updateMap qn newmeta; autos := autos; next $= 1 +] mc
+  setMetaContext $ { metas $= updateMap qn newmeta; autos := autos; next $= 1 +} mc
 
   -- I tried checking Auto immediately if CheckAll, but there isn't enough information yet.
   pure $ applyBDs 0 (Meta fc qn) ctx.bds
diff --git a/src/Lib/ProcessModule.newt b/src/Lib/ProcessModule.newt
index c156752..650b909 100644
--- a/src/Lib/ProcessModule.newt
+++ b/src/Lib/ProcessModule.newt
@@ -17,13 +17,13 @@ import Lib.Elab
 -- declare internal primitives
 addPrimitives : M ModContext
 addPrimitives = do
-  modifyTop [ currentMod := emptyModCtx "Prim" ""; hints := emptyMap; ops := emptyMap ]
+  modifyTop { currentMod := emptyModCtx "Prim" ""; hints := emptyMap; ops := emptyMap }
   processDecl primNS (PType emptyFC "Int" Nothing)
   processDecl primNS (PType emptyFC "String" Nothing)
   processDecl primNS (PType emptyFC "Char" Nothing)
   setDef (QN primNS "PiType") emptyFC (Erased emptyFC) (PrimFn "(h0, h1) => ({ tag: \"PiType\", h0, h1 });" (S (S Z)) Nil) Nil
   top <- getTop
-  modifyTop [ modules $= updateMap primNS top.currentMod ]
+  modifyTop { modules $= updateMap primNS top.currentMod }
   pure top.currentMod
 
 record FileSource where
@@ -74,12 +74,12 @@ processModule importFC repo stk modns = do
 
   -- Dummy for initial load/parse
   let mod = MkModCtx modns "" emptyMap freshMC emptyMap Nil Nil Nil
-  modifyTop [ currentMod := mod; hints := emptyMap; ops := emptyMap ]
+  modifyTop { currentMod := mod; hints := emptyMap; ops := emptyMap }
 
   -- TODO now we can pass in the module name...
   Right (fn,src) <- tryError $ repo.getFile importFC fn
     | Left err => reportError err  -- TODO maybe want a better FC.
-  modifyTop [ currentMod $= [ modSource := src ]]
+  modifyTop { currentMod $= { modSource := src }}
 
   let (Right toks) = tokenise fn src
     | Left err => reportError err
@@ -108,10 +108,10 @@ processModule importFC repo stk modns = do
   -- currentMod has been wiped by imports..
   let freshMC = MC emptyMap Nil 0 CheckAll
   let mod = MkModCtx modns src emptyMap freshMC emptyMap imported Nil Nil
-  modifyTop [ currentMod := mod
+  modifyTop { currentMod := mod
             ; hints := emptyMap
             ; ops := ops
-            ]
+            }
 
   -- top hints / ops include all directly imported modules
   top <- getTop
@@ -119,7 +119,7 @@ processModule importFC repo stk modns = do
     (MkImport fc (nameFC, ns)) => do
       let (Just mod) = lookupMap' ns top.modules | _ => error emptyFC "namespace \{show ns} missing"
       importHints (listValues mod.modDefs)
-      modifyTop [ ops $= mergeOps mod.modOps ]
+      modifyTop { ops $= mergeOps mod.modOps }
 
       -- add error if an import contains an error
       -- maybe move this to after reporting
@@ -135,7 +135,7 @@ processModule importFC repo stk modns = do
   -- aside from reworking parsing, we could filter
   -- other options are removing updates from parsing (so we must use incremental parsing)
   -- or removing pratt from parsing (so it happens in elaboration)
-  modifyTop [ currentMod $= [ modOps := ops ] ]
+  modifyTop { currentMod $= { modOps := ops } }
 
   log 1 $ \ _ => "process Decls"
   traverse (tryProcessDecl src modns) (collectDecl decls)
@@ -151,7 +151,7 @@ processModule importFC repo stk modns = do
   -- update modules with result, leave the rest of context in case this is top file
   top <- getTop
   let modules = updateMap modns top.currentMod top.modules
-  modifyTop [modules := modules]
+  modifyTop {modules := modules}
 
   pure top.currentMod
   where
@@ -159,7 +159,7 @@ processModule importFC repo stk modns = do
     reportError err = do
       addError err
       top <- getTop
-      modifyTop [modules $= updateMap modns top.currentMod ]
+      modifyTop {modules $= updateMap modns top.currentMod }
       pure top.currentMod
 
     tryProcessDecl : String → String → Decl → M Unit
@@ -174,7 +174,7 @@ invalidateModule modname = do
   let modules = join $ map getDeps $ toList top.modules
   let revMap = map swap modules
   let deps = foldl accumulate emptyMap revMap
-  modifyTop [ modules $= go deps (modname :: Nil) ]
+  modifyTop { modules $= go deps (modname :: Nil) }
   where
     accumulate : SortedMap String (List String) → String × String → SortedMap String (List String)
     accumulate deps (k,v) = let prev = fromMaybe Nil $ lookupMap' k deps
diff --git a/src/Lib/TopContext.newt b/src/Lib/TopContext.newt
index 20e2964..660ed51 100644
--- a/src/Lib/TopContext.newt
+++ b/src/Lib/TopContext.newt
@@ -53,7 +53,7 @@ setFlag name fc flag = do
   top <- getTop
   let (Just (MkEntry fc nm ty def flags)) = lookupMap' name top.currentMod.modDefs
     | Nothing => error fc "\{show name} not declared"
-  modifyTop [ currentMod $= [ modDefs $= (updateMap name (MkEntry fc name ty def (flag :: flags)))] ]
+  modifyTop { currentMod $= { modDefs $= (updateMap name (MkEntry fc name ty def (flag :: flags)))} }
 
 setDef : QName -> FC -> Tm -> Def → List EFlag -> M Unit
 setDef name fc ty def flags = do
@@ -61,14 +61,14 @@ setDef name fc ty def flags = do
   let (Nothing) = lookupMap' name top.currentMod.modDefs
     | Just (MkEntry fc' nm' ty' def' _) => error fc "\{show name} is already defined at \{show fc'}"
 
-  modifyTop [currentMod $= [ modDefs $= (updateMap name (MkEntry fc name ty def flags))] ]
+  modifyTop {currentMod $= { modDefs $= (updateMap name (MkEntry fc name ty def flags))} }
 
 updateDef : QName -> FC -> Tm -> Def -> M Unit
 updateDef name fc ty def = do
   top <- getTop
   let (Just (MkEntry fc' nm' ty' def' flags)) = lookupMap' name top.currentMod.modDefs
     | Nothing => error fc "\{show name} not declared"
-  modifyTop [ currentMod $= [ modDefs := updateMap name (MkEntry fc' name ty def flags) top.currentMod.modDefs ] ]
+  modifyTop { currentMod $= { modDefs := updateMap name (MkEntry fc' name ty def flags) top.currentMod.modDefs } }
 
 typeName : Tm → Maybe QName
 typeName (Pi fc nm Explicit rig t u) = Nothing
@@ -86,18 +86,18 @@ addHint qn = do
         | Nothing => error entry.fc "can't find tcon name for \{show qn}"
       let xs = fromMaybe Nil $ lookupMap' tyname top.hints
       let hints = updateMap tyname ((qn, entry.type) :: xs) top.hints
-      modifyTop [ hints := hints ]
+      modifyTop { hints := hints }
     Nothing => pure MkUnit
 
 addError : Error -> M Unit
-addError err = modifyTop [ currentMod $= [ modErrors $= (err ::) ] ]
+addError err = modifyTop { currentMod $= { modErrors $= (err ::) } }
 
 addInfo : EditorInfo → M Unit
-addInfo info = modifyTop [ currentMod $= [modInfos $= (info ::) ] ]
+addInfo info = modifyTop { currentMod $= {modInfos $= (info ::) } }
 
 -- temporary? used in derive for now
 freshName : String → M String
 freshName nm = do
   top <- getTop
-  modifyTop [ freshIx $= 1 + ]
+  modifyTop { freshIx $= 1 + }
   pure $ "f$" ++ nm ++ show top.freshIx
diff --git a/src/Main.newt b/src/Main.newt
index 8e17371..66540da 100644
--- a/src/Main.newt
+++ b/src/Main.newt
@@ -114,7 +114,7 @@ cmdLine : List String -> M (Maybe String × List String)
 cmdLine Nil = pure (Nothing, Nil)
 cmdLine ("--top" :: args) = cmdLine args -- handled later
 cmdLine ("-v" :: args) = do
-  modifyTop [ verbose $= _+_ 1 ]
+  modifyTop { verbose $= _+_ 1 }
   cmdLine args
 cmdLine ("-o" :: fn :: args) = do
   (out, files) <- cmdLine args
@@ -166,8 +166,8 @@ runCommand (Load fn) = processFile fn
 runCommand (HelpCmd) = replHelp
 runCommand (BrowseCmd qn) = browseTop qn
 runCommand (GetDoc name) = getDoc name
-runCommand (Verbose Nothing) = modifyTop [ verbose $= _+_ 1 ]
-runCommand (Verbose (Just v)) = modifyTop [ verbose := v ]
+runCommand (Verbose Nothing) = modifyTop { verbose $= _+_ 1 }
+runCommand (Verbose (Just v)) = modifyTop { verbose := v }
 runCommand (OutputJS fn) = writeSource fn
 runCommand DumpTop = do
   json <- jsonTopContext