diff --git a/REPL/Extract/Declaration.lean b/REPL/Extract/Declaration.lean
new file mode 100644
index 00000000..236cfcd7
--- /dev/null
+++ b/REPL/Extract/Declaration.lean
@@ -0,0 +1,231 @@
+import REPL.JSON
+
+open Lean Elab System Parser
+
+namespace REPL
+
+/-! Extract information about declarations from info trees
+Inspired by <https://github.com/frenzymath/jixia>
+-/
+
+/-- See `Lean.Parser.Command.declModifiers` and `Lean.Elab.elabModifiers` -/
+def getModifiers (stx : Syntax) (ctx: ContextInfo): DeclModifiers :=
+  match stx with
+  | .node _ ``Command.declModifiers _ =>
+    { docString := stx[0].getOptional?.map (fun stx =>
+        { content := stx.prettyPrint.pretty, range := stx.toRange ctx }),
+      visibility := (stx[2].getOptional?.map (·.prettyPrint.pretty.trimAscii.toString)).getD "regular",
+      computeKind := (stx[4].getOptional?.map (·.prettyPrint.pretty.trimAscii.toString)).getD "regular",
+      isProtected := !stx[3].isNone,
+      isUnsafe := !stx[5].isNone,
+      recKind := (stx[6].getOptional?.map (·.prettyPrint.pretty.trimAscii.toString)).getD "default",
+      attributes := stx[1].getArgs.toList.flatMap parseAttributes, }
+  | _ => {}
+  where
+    /-- Parse attribute instances from a Term.attributes syntax node
+    See `Lean.Parser.Term.attributes`.
+    -/
+    parseAttributes (attrSyntax : Syntax) : List String :=
+      match attrSyntax with
+      | .node _ ``Term.attributes args =>
+        -- args[0] is "@[", args[1] is the attribute list, args[2] is "]"
+        if args.size > 1 then
+          args[1]!.getArgs.toList.flatMap fun inst =>
+            match inst with
+            | .node _ ``Term.attrInstance _ => [inst.prettyPrint.pretty.trimAscii.toString]
+            | _ => []
+        else []
+      | _ => []
+
+partial def getIdents (stx : Syntax) : Array Name :=
+  match stx with
+  | .node _ _ args => args.flatMap getIdents
+  | .ident _ _ id _ => #[id]
+  | _ => #[]
+
+/-- See `Lean.Elab.Term.toBinderViews` -/
+def toBinderViews (stx : Syntax) : Array BinderView :=
+  let k := stx.getKind
+  if stx.isIdent || k == ``Term.hole then
+    -- binderIdent
+    #[{ id := (expandBinderIdent stx), type := mkHole stx, binderInfo := "default" }]
+  else if k == ``Lean.Parser.Term.explicitBinder then
+    -- `(` binderIdent+ binderType (binderDefault <|> binderTactic)? `)`
+    let ids := getBinderIds stx[1]
+    let type        := stx[2]
+    -- let optModifier := stx[3]
+    ids.map fun id => { id := (expandBinderIdent id), type := (expandBinderType id type), binderInfo := "default" }
+  else if k == ``Lean.Parser.Term.implicitBinder then
+    -- `{` binderIdent+ binderType `}`
+    let ids := getBinderIds stx[1]
+    let type := stx[2]
+    ids.map fun id => { id := (expandBinderIdent id), type := (expandBinderType id type), binderInfo := "implicit" }
+  else if k == ``Lean.Parser.Term.strictImplicitBinder then
+    -- `⦃` binderIdent+ binderType `⦄`
+    let ids := getBinderIds stx[1]
+    let type := stx[2]
+    ids.map fun id => { id := (expandBinderIdent id), type := (expandBinderType id type), binderInfo := "strictImplicit" }
+  else if k == ``Lean.Parser.Term.instBinder then
+    -- `[` optIdent type `]`
+    let id := expandOptIdent stx[1]
+    let type := stx[2]
+    #[ { id := id, type := type, binderInfo := "instImplicit" } ]
+  else
+    #[]
+  where
+    getBinderIds (ids : Syntax) : Array Syntax :=
+      ids.getArgs.map fun (id : Syntax) =>
+        let k := id.getKind
+        if k == identKind || k == `Lean.Parser.Term.hole then id
+        else Syntax.missing
+    expandBinderType (ref : Syntax) (stx : Syntax) : Syntax :=
+      if stx.getNumArgs == 0 then mkHole ref else stx[1]
+    expandBinderIdent (stx : Syntax) : Syntax :=
+      match stx with
+      | `(_) => Syntax.missing
+      | _    => stx
+    expandOptIdent (stx : Syntax) : Syntax :=
+      if stx.isNone then Syntax.missing else stx[0]
+
+def getScope (ctx : ContextInfo) (state : Command.State) : ScopeInfo :=
+  let scope := state.scopes.head!
+  {
+    varDecls := scope.varDecls.map fun stx => s!"variable {stx.raw.prettyPrint.pretty}",
+    includeVars := scope.includedVars.toArray.map fun name => name.eraseMacroScopes,
+    omitVars := scope.omittedVars.toArray.map fun name => name.eraseMacroScopes,
+    levelNames := scope.levelNames.toArray,
+    currNamespace := ctx.currNamespace,
+    openDecl := ctx.openDecls,
+  }
+
+partial def extractDeclarationInfo (cmdInfo : CommandInfo) (infoTree : InfoTree) (ctx : ContextInfo)
+  (prevState : Command.State) : DeclarationInfo :=
+  let stx := cmdInfo.stx
+  let modifiers := getModifiers stx[0] ctx
+  let decl := stx[1]
+  let kind := decl.getKind
+  let kindStr := match kind with
+    | .str _ s => s
+    | _ => kind.toString
+
+  -- See `Lean.Elab.DefView`
+  let (signature, id, binders, type?, value?) := match kind with
+    | ``Command.abbrev
+    | ``Command.definition =>
+      let (binders, type) := expandOptDeclSig decl[2]
+      (decl[2], decl[1], binders, type, some decl[3])
+    | ``Command.theorem =>
+      let (binders, type) := expandDeclSig decl[2]
+      (decl[2], decl[1], binders, some type, some decl[3])
+    | ``Command.opaque =>
+      let (binders, type) := expandDeclSig decl[2]
+      (decl[2], decl[1], binders, some type, decl[3].getOptional?)
+    | ``Command.axiom =>
+      let (binders, type) := expandDeclSig decl[2]
+      (decl[2], decl[1], binders, some type, none)
+    | ``Command.inductive
+    | ``Command.classInductive =>
+      let (binders, type) := expandOptDeclSig decl[2]
+      (decl[2], decl[1], binders, type, some decl[4])
+    | ``Command.instance =>
+      let (binders, type) := expandDeclSig decl[4]
+      let declId := match stx[3].getOptional? with
+        | some declId => declId
+        | none        => Syntax.missing -- TODO: improve this
+      (decl[4], declId, binders, some type, some decl[5])
+    | ``Command.example =>
+      let id              := mkIdentFrom stx[0] `_example (canonical := true)
+      let declId          := mkNode ``Parser.Command.declId #[id, mkNullNode]
+      let (binders, type) := expandOptDeclSig decl[1]
+      (decl[1], declId, binders, type, some decl[2])
+    | ``Command.structure =>
+      let signature := Syntax.node2 .none ``Command.optDeclSig decl[2] decl[4]
+      let (binders, type) := (decl[2], some decl[4])
+      (signature, decl[1], binders, type, none)
+    | _ => unreachable!
+
+  let name := id[0].getId
+  let fullName := match getFullname infoTree name with -- TODO: could be better
+    | [] => name
+    | a :: _  => a
+
+  let binders : Option DeclBinders := match binders.getArgs with
+    | #[] => none
+    | _ => some { pp := binders.prettyPrint.pretty,
+                  groups := binders.getArgs.map (·.prettyPrint.pretty),
+                  map := binders.getArgs.flatMap toBinderViews,
+                  range := binders.toRange ctx }
+
+  -- let a := prevState.env.constants.find! decl[1].getId
+  -- a.getUsedConstantsAsSet
+
+  let extractConstants (stx : Syntax) : Array Name := -- TODO: improve this
+    let idents := ((getIdents stx).foldl
+      (init := NameSet.empty) fun acc name => acc.insert name).toArray
+    idents
+    -- idents.filter prevState.env.constants.contains
+
+  {
+    pp := stx.prettyPrint.pretty,
+    name,
+    fullName,
+    kind := kindStr,
+    modifiers,
+    scope := getScope ctx prevState,
+    signature := { pp := signature.prettyPrint.pretty,
+                    constants := extractConstants signature,
+                    range := signature.toRange ctx },
+    binders,
+    type := type?.map fun t =>
+      { pp := t.prettyPrint.pretty, constants := extractConstants t, range := t.toRange ctx },
+    value := value?.map fun v =>
+      { pp := v.prettyPrint.pretty, constants := extractConstants v, range := v.toRange ctx },
+    range := stx.toRange ctx
+  }
+where
+  getFullname (infoTree : InfoTree) (shortName : Name) : List Name :=
+    match infoTree with
+    | .context _ t => getFullname t shortName
+    | .node i ts  =>
+      match i with
+        | .ofTermInfo ti => ti.expr.constName?.toList.filter (fun n =>
+              match shortName.componentsRev with
+              | [] => true
+              | h :: _ => match n.componentsRev with
+                | [] => false
+                | h' :: _ => h == h'
+            )
+        | _ => ts.toList.flatMap (getFullname · shortName)
+    | _ => []
+
+open Lean.Parser in
+/-- Extract all declarations from InfoTrees -/
+partial def extractCmdDeclarationInfos (trees : List InfoTree) (prevState : Command.State) :
+    List DeclarationInfo :=
+  let allDecls := trees.map (extractFromTree · none prevState)
+  allDecls.flatten
+where
+  extractFromTree (t : InfoTree) (ctx? : Option ContextInfo) (prevState : Command.State) :
+      List DeclarationInfo :=
+    match t with
+    | .context ctx t => extractFromTree t (ctx.mergeIntoOuter? ctx?) prevState
+    | .node i ts =>
+      match i with
+      | .ofCommandInfo cmdInfo =>
+        match ctx? with
+        | some ctx =>
+          if cmdInfo.stx.getKind == ``Command.declaration then
+            [extractDeclarationInfo cmdInfo t ctx prevState]
+          else
+            ts.toList.flatMap (extractFromTree · ctx? prevState)
+        | none => ts.toList.flatMap (extractFromTree · ctx? prevState)
+      | _ => ts.toList.flatMap (extractFromTree · ctx? prevState)
+    | _ => []
+
+def extractAllDeclarationInfos (treeList : List (IncrementalState × Option InfoTree)) (prevState : Command.State) : List DeclarationInfo :=
+  match treeList with
+  | [] => []
+  | (state, infoTree?) :: rest =>
+    let decls := extractCmdDeclarationInfos infoTree?.toList prevState
+    let restDecls := extractAllDeclarationInfos rest state.commandState
+    decls ++ restDecls
diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean
index 81575ed3..20885db9 100644
--- a/REPL/Frontend.lean
+++ b/REPL/Frontend.lean
@@ -4,11 +4,44 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Lean.Elab.Frontend
+import Std.Data.HashMap
 
-open Lean Elab
+open Lean Elab Language
 
 namespace Lean.Elab.IO
 
+partial def IO.processCommandsIncrementally' (inputCtx : Parser.InputContext)
+    (parserState : Parser.ModuleParserState) (commandState : Command.State)
+    (old? : Option IncrementalState) :
+    BaseIO (List (IncrementalState × Option InfoTree)) := do
+  let task ← Language.Lean.processCommands inputCtx parserState commandState
+    (old?.map fun old => (old.inputCtx, old.initialSnap))
+  return go task.get task #[]
+where
+  go initialSnap t commands :=
+    let snap := t.get
+    let commands := commands.push snap
+    -- Opting into reuse also enables incremental reporting, so make sure to collect messages from
+    -- all snapshots
+    let messages := toSnapshotTree initialSnap
+      |>.getAll.map (·.diagnostics.msgLog)
+      |>.foldl (· ++ ·) {}
+    -- In contrast to messages, we should collect info trees only from the top-level command
+    -- snapshots as they subsume any info trees reported incrementally by their children.
+    let trees := commands.map (·.elabSnap.infoTreeSnap.get.infoTree?) |>.filterMap id |>.toPArray'
+    let result : (IncrementalState × Option InfoTree) :=
+      ({ commandState := { snap.elabSnap.resultSnap.get.cmdState with messages, infoState.trees := trees }
+         , parserState := snap.parserState
+         , cmdPos := snap.parserState.pos
+         , commands := commands.map (·.stx)
+         , inputCtx := inputCtx
+         , initialSnap := initialSnap
+       }, snap.elabSnap.infoTreeSnap.get.infoTree?)
+    if let some next := snap.nextCmdSnap? then
+      result :: go initialSnap next.task commands
+    else
+      [result]
+
 /--
 Wrapper for `IO.processCommands` that enables info states, and returns
 * the new command state
@@ -17,41 +50,48 @@ Wrapper for `IO.processCommands` that enables info states, and returns
 -/
 def processCommandsWithInfoTrees
     (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)
-    (commandState : Command.State) : IO (Command.State × List Message × List InfoTree) := do
+    (commandState : Command.State) (incrementalState? : Option IncrementalState := none)
+    : IO (List (IncrementalState × Option InfoTree) × List Message) := do
   let commandState := { commandState with infoState.enabled := true }
-  let s ← IO.processCommands inputCtx parserState commandState <&> Frontend.State.commandState
-  pure (s, s.messages.toList, s.infoState.trees.toList)
+  let incStates ← IO.processCommandsIncrementally' inputCtx parserState commandState incrementalState?
+  pure (incStates, (incStates.getLast?.map (·.1.commandState.messages.toList)).getD {})
 
 /--
 Process some text input, with or without an existing command state.
-If there is no existing environment, we parse the input for headers (e.g. import statements),
-and create a new environment.
-Otherwise, we add to the existing environment.
+Supports header caching to avoid reprocessing the same imports repeatedly.
 
 Returns:
-1. The header-only command state (only useful when cmdState? is none)
-2. The resulting command state after processing the entire input
-3. List of messages
-4. List of info trees
+1. The resulting command state after processing the entire input
+2. List of messages
+3. List of info trees along with Command.State from the incremental processing
+4. Updated header cache mapping import keys to Command.State
 -/
 def processInput (input : String) (cmdState? : Option Command.State)
+    (incrementalState? : Option IncrementalState := none)
+    (headerCache : Std.HashMap String Command.State)
     (opts : Options := {}) (fileName : Option String := none) :
-    IO (Command.State × Command.State × List Message × List InfoTree) := unsafe do
+    IO (Command.State × List (IncrementalState × Option InfoTree) × List Message × (Std.HashMap String Command.State)) := unsafe do
   Lean.initSearchPath (← Lean.findSysroot)
   enableInitializersExecution
   let fileName   := fileName.getD "<input>"
   let inputCtx   := Parser.mkInputContext input fileName
-
   match cmdState? with
   | none => do
-    -- Split the processing into two phases to prevent self-reference in proofs in tactic mode
     let (header, parserState, messages) ← Parser.parseHeader inputCtx
-    let (env, messages) ← processHeader header opts messages inputCtx
-    let headerOnlyState := Command.mkState env messages opts
-    let (cmdState, messages, trees) ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState
-    return (headerOnlyState, cmdState, messages, trees)
-
+    let importKey := toString header.raw -- do not contain comments and whitespace
+    match headerCache.get? importKey with
+    | some cachedHeaderState => do
+      -- Header is cached, use it as the base command state
+      let (incStates, messages) ← processCommandsWithInfoTrees inputCtx parserState cachedHeaderState incrementalState?
+      return (cachedHeaderState, incStates, messages, headerCache)
+    | none => do
+      -- Header not cached, process it and cache the result
+      let (env, messages) ← processHeader header opts messages inputCtx
+      let headerOnlyState := Command.mkState env messages opts
+      let headerCache := headerCache.insert importKey headerOnlyState
+      let (incStates, messages) ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState incrementalState?
+      return (headerOnlyState, incStates, messages, headerCache)
   | some cmdStateBefore => do
     let parserState : Parser.ModuleParserState := {}
-    let (cmdStateAfter, messages, trees) ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore
-    return (cmdStateBefore, cmdStateAfter, messages, trees)
+    let (incStates, messages) ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore incrementalState?
+    return (cmdStateBefore, incStates, messages, headerCache)
diff --git a/REPL/JSON.lean b/REPL/JSON.lean
index aaeec551..cb2f7724 100644
--- a/REPL/JSON.lean
+++ b/REPL/JSON.lean
@@ -6,6 +6,7 @@ Authors: Scott Morrison
 import Lean.Data.Json
 import Lean.Message
 import Lean.Elab.InfoTree.Main
+import REPL.Lean.InfoTree.ToJson
 
 open Lean Elab InfoTree
 
@@ -13,12 +14,14 @@ namespace REPL
 
 structure CommandOptions where
   allTactics : Option Bool := none
+  declarations: Option Bool := none
   rootGoals : Option Bool := none
   /--
   Should be "full", "tactics", "original", or "substantive".
   Anything else is ignored.
   -/
   infotree : Option String
+  incrementality : Option Bool := none -- whether to use incremental mode optimization
 
 /-- Run Lean commands.
 If `env = none`, starts a new session (in which you can use `import`).
@@ -47,7 +50,7 @@ deriving ToJson, FromJson
 structure Pos where
   line : Nat
   column : Nat
-deriving ToJson, FromJson
+deriving ToJson, FromJson, BEq, Hashable
 
 /-- Severity of a message. -/
 inductive Severity
@@ -117,6 +120,92 @@ def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState :
     proofState,
     usedConstants }
 
+structure DocString where
+  content : String
+  range : Elab.Syntax.Range
+deriving ToJson
+
+/-- See `Lean.Elab.Modifiers` -/
+structure DeclModifiers where
+  docString : Option DocString := none
+  visibility : String := "regular" -- "regular", "private", or "public"
+  computeKind : String := "regular" -- "regular", "meta", or "noncomputable"
+  recKind : String := "default" -- "default", "partial", or "nonrec"
+  isProtected : Bool := false
+  isUnsafe : Bool := false
+  attributes : List String := []
+deriving ToJson
+
+structure DeclSignature where
+  pp : String
+  constants : Array Name
+  range : Elab.Syntax.Range
+deriving ToJson
+
+structure BinderView where
+  id   : Syntax
+  type : Syntax
+  binderInfo : String
+
+instance : ToJson BinderView where
+  toJson (bv : BinderView) : Json :=
+    Json.mkObj [
+      ("id", toString bv.id.prettyPrint),
+      ("type", toString bv.type.prettyPrint),
+      ("binderInfo", bv.binderInfo)
+    ]
+
+structure DeclBinders where
+  pp : String
+  groups : Array String
+  map : Array BinderView
+  range : Elab.Syntax.Range
+deriving ToJson
+
+structure DeclType where
+  pp : String
+  constants : Array Name
+  range : Elab.Syntax.Range
+deriving ToJson
+
+structure DeclValue where
+  pp : String
+  constants : Array Name
+  range : Elab.Syntax.Range
+deriving ToJson
+
+local instance : ToJson OpenDecl where
+  toJson
+  | .simple ns except => json%{
+    simple: { «namespace»: $ns, except: $except }
+  }
+  | .explicit id declName => json%{
+    rename: { name: $declName, as: $id }
+  }
+
+structure ScopeInfo where
+  varDecls : Array String
+  includeVars : Array Name
+  omitVars : Array Name
+  levelNames : Array Name
+  currNamespace : Name
+  openDecl : List OpenDecl
+deriving ToJson
+
+structure DeclarationInfo where
+  pp: String
+  range : Elab.Syntax.Range
+  scope : ScopeInfo
+  name : Name
+  fullName : Name
+  kind : String
+  modifiers : DeclModifiers
+  signature: DeclSignature
+  binders : Option DeclBinders := none
+  type : Option DeclType := none
+  value : Option DeclValue := none
+deriving ToJson
+
 /--
 A response to a Lean command.
 `env` can be used in later calls, to build on the stored environment.
@@ -126,8 +215,8 @@ structure CommandResponse where
   messages : List Message := []
   sorries : List Sorry := []
   tactics : List Tactic := []
+  declarations: List DeclarationInfo := []
   infotree : Option Json := none
-deriving FromJson
 
 def Json.nonemptyList [ToJson α] (k : String) : List α → List (String × Json)
   | [] => []
@@ -139,6 +228,7 @@ instance : ToJson CommandResponse where
     Json.nonemptyList "messages" r.messages,
     Json.nonemptyList "sorries" r.sorries,
     Json.nonemptyList "tactics" r.tactics,
+    Json.nonemptyList "declarations" r.declarations,
     match r.infotree with | some j => [("infotree", j)] | none => []
   ]
 
diff --git a/REPL/Main.lean b/REPL/Main.lean
index 9b36b27d..6e2c21da 100644
--- a/REPL/Main.lean
+++ b/REPL/Main.lean
@@ -6,11 +6,15 @@ Authors: Scott Morrison
 import REPL.JSON
 import REPL.Frontend
 import REPL.Util.Path
+import REPL.Extract.Declaration
 import REPL.Lean.ContextInfo
 import REPL.Lean.Environment
 import REPL.Lean.InfoTree
 import REPL.Lean.InfoTree.ToJson
 import REPL.Snapshots
+import REPL.Util.Trie
+import Lean.Data.Trie
+import Std.Data.HashMap
 
 /-!
 # A REPL for Lean.
@@ -72,6 +76,16 @@ structure State where
   and report the numerical index for the recorded state at each sorry.
   -/
   proofStates : Array ProofSnapshot := #[]
+  /--
+  Trie-based storage for fast prefix matching, organized by environment ID.
+  Map from environment ID (None for fresh env) to trie of command prefixes with incremental states.
+  -/
+  envTries : Std.HashMap (Option Nat) (Lean.Data.Trie IncrementalState) := Std.HashMap.emptyWithCapacity 8
+  /--
+  Cache for processed headers (import statements) to avoid reprocessing the same imports repeatedly.
+  Maps import raw string to the processed command state.
+  -/
+  headerCache : Std.HashMap String Command.State := Std.HashMap.emptyWithCapacity 8
 
 /--
 The Lean REPL monad.
@@ -88,12 +102,43 @@ def recordCommandSnapshot (state : CommandSnapshot) : M m Nat := do
   modify fun s => { s with cmdStates := s.cmdStates.push state }
   return id
 
+/-- Add all incremental states of a command to the trie at their corresponding prefix positions -/
+def addCommandToTrie (cmdText : String)
+    (incStates : List (IncrementalState × Option InfoTree)) (envId? : Option Nat) : M m Unit := do
+  let state ← get
+  let currentTrie := state.envTries.get? envId? |>.getD Lean.Data.Trie.empty
+
+  let mut newTrie := currentTrie
+  for (incState, _) in incStates do
+    let prefixPos := incState.cmdPos.byteIdx
+    let cmdPrefix : String := (cmdText.take prefixPos).trimAscii.toString
+    newTrie := REPL.Util.Trie.insert newTrie cmdPrefix incState
+
+  modify fun s => { s with envTries := s.envTries.insert envId? newTrie }
+
+/-- Record command text and incremental states for prefix matching reuse. -/
+def recordCommandIncrementals (cmdText : String)
+    (incStates : List (IncrementalState × Option InfoTree)) (envId? : Option Nat) : M m Unit := do
+  addCommandToTrie cmdText incStates envId?
+
 /-- Record a `ProofSnapshot` into the REPL state, returning its index for future use. -/
 def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat := do
   let id := (← get).proofStates.size
   modify fun s => { s with proofStates := s.proofStates.push proofState }
   return id
 
+/-- Find the best incremental state using trie-based prefix matching -/
+def findBestIncrementalState (newCmd : String) (envId? : Option Nat) : M m (Option IncrementalState) := do
+  let state ← get
+  let trimmedCmd := newCmd.trimAscii.toString
+  let trie? := state.envTries.get? envId?
+  match trie? with
+  | none => return none
+  | some trie =>
+    match REPL.Util.Trie.matchPrefix trie trimmedCmd 0 with
+    | some incState => return some incState
+    | none => return none
+
 def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Option (List MVarId))
 : M m (List Sorry) :=
   trees.flatMap InfoTree.sorries |>.filter (fun t => match t.2.1 with
@@ -102,11 +147,7 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op
       fun ⟨ctx, g, pos, endPos⟩ => do
         let (goal, proofState) ← match g with
         | .tactic g => do
-          let lctx ← ctx.runMetaM {} do
-              match ctx.mctx.findDecl? g with
-              | some decl => return decl.lctx
-              | none => throwError "unknown metavariable '{g}'"
-          let s ← ProofSnapshot.create ctx lctx env? [g] rootGoals?
+          let s ← ProofSnapshot.create ctx none env? [g] rootGoals?
           pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
         | .term lctx (some t) => do
           let s ← ProofSnapshot.create ctx lctx env? [] rootGoals? [t]
@@ -115,6 +156,16 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op
         let proofStateId ← proofState.mapM recordProofSnapshot
         return Sorry.of goal pos endPos proofStateId
 
+def sorriesCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment)
+(rootGoals? : Option (List MVarId))
+: M m (List Sorry) :=
+  match treeList with
+  | [] => pure []
+  | (state, infoTree?) :: rest => do
+    let s ← sorries infoTree?.toList prevEnv rootGoals?
+    let restSorries ← sorriesCmd rest state.commandState.env rootGoals?
+    return s ++ restSorries
+
 def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format :=
   ctx.runMetaM {} try
     Lean.PrettyPrinter.ppTactic ⟨stx⟩
@@ -130,6 +181,14 @@ def tactics (trees : List InfoTree) (env? : Option Environment) : M m (List Tact
       let proofStateId ← proofState.mapM recordProofSnapshot
       return Tactic.of goals tactic pos endPos proofStateId ns
 
+def tacticsCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment) : M m (List Tactic) := do
+  match treeList with
+  | [] => pure []
+  | (state, infoTree?) :: rest => do
+    let ts ← tactics infoTree?.toList prevEnv
+    let restTactics ← tacticsCmd rest state.commandState.env
+    return ts ++ restTactics
+
 def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do
   trees.flatMap InfoTree.rootGoals |>.mapM
     fun ⟨ctx, goals, pos⟩ => do
@@ -138,6 +197,14 @@ def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment
       let proofStateId ← proofState.mapM recordProofSnapshot
       return Sorry.of goals pos pos proofStateId
 
+def collectRootGoalsAsSorriesCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment) :
+    M m (List Sorry) := do
+  match treeList with
+  | [] => pure []
+  | (state, infoTree?) :: rest => do
+    let sorries ← collectRootGoalsAsSorries infoTree?.toList prevEnv
+    let restSorries ← collectRootGoalsAsSorriesCmd rest state.commandState.env
+    return sorries ++ restSorries
 
 private def collectFVarsAux : Expr → NameSet
   | .fvar fvarId => NameSet.empty.insert fvarId.name
@@ -197,7 +264,7 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do
             unless (← Meta.isDefEq pft expectedType) do
               return s!"Error: proof has type {pft} but root goal has type {expectedType}"
 
-            let pf ← abstractAllLambdaFVars pf
+            let pf ← abstractAllLambdaFVars pf >>= instantiateMVars
             let pft ← Meta.inferType pf >>= instantiateMVars
 
             if pf.hasExprMVar then
@@ -302,20 +369,33 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
   if notFound then
     return .inr ⟨"Unknown environment."⟩
   let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState
-  let (initialCmdState, cmdState, messages, trees) ← try
-    IO.processInput s.cmd initialCmdState?
+
+  let (initialCmdState, incStates, messages) ← try
+    if s.incrementality.getD false then
+      let bestIncrementalState? ← findBestIncrementalState s.cmd s.env
+      let (initialCmdState, incStates, messages, headerCache) ← IO.processInput s.cmd initialCmdState? bestIncrementalState? (← get).headerCache
+      -- Store the command text and incremental states for future reuse
+      modify fun st => { st with headerCache := headerCache }
+      recordCommandIncrementals s.cmd incStates s.env
+      pure (initialCmdState, incStates, messages)
+    else
+      let (initialCmdState, incStates, messages, _) ← IO.processInput s.cmd initialCmdState? none {}
+      pure (initialCmdState, incStates, messages)
   catch ex =>
     return .inr ⟨ex.toString⟩
+
+  let cmdState := (incStates.getLast?.map (fun c => c.1.commandState)).getD initialCmdState
   let messages ← messages.mapM fun m => Message.of m
-  -- For debugging purposes, sometimes we print out the trees here:
-  -- trees.forM fun t => do IO.println (← t.format)
-  let sorries ← sorries trees initialCmdState.env none
+  let sorries ← sorriesCmd incStates initialCmdState.env none
   let sorries ← match s.rootGoals with
-  | some true => pure (sorries ++ (← collectRootGoalsAsSorries trees initialCmdState.env))
+  | some true => pure (sorries ++ (← collectRootGoalsAsSorriesCmd incStates initialCmdState.env))
   | _ => pure sorries
   let tactics ← match s.allTactics with
-  | some true => tactics trees initialCmdState.env
+  | some true => tacticsCmd incStates initialCmdState.env
   | _ => pure []
+  let declarations := match s.declarations with
+  | some true => extractAllDeclarationInfos incStates initialCmdState
+  | _ => []
   let cmdSnapshot :=
   { cmdState
     cmdContext := (cmdSnapshot?.map fun c => c.cmdContext).getD
@@ -324,6 +404,9 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
         snap? := none,
         cancelTk? := none } }
   let env ← recordCommandSnapshot cmdSnapshot
+  let trees := cmdState.infoState.trees.toList
+  -- For debugging purposes, sometimes we print out the trees here:
+  -- trees.forM fun t => do IO.println (← t.format)
   let jsonTrees := match s.infotree with
   | some "full" => trees
   | some "tactics" => trees.flatMap InfoTree.retainTacticInfo
@@ -338,7 +421,8 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
     { env,
       messages,
       sorries,
-      tactics
+      tactics,
+      declarations,
       infotree }
 
 def processFile (s : File) : M IO (CommandResponse ⊕ Error) := do
diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean
index eaebffc4..b5597a40 100644
--- a/REPL/Snapshots.lean
+++ b/REPL/Snapshots.lean
@@ -185,33 +185,44 @@ def runString (p : ProofSnapshot) (t : String) : IO ProofSnapshot :=
 /-- Pretty print the current goals in the `ProofSnapshot`. -/
 def ppGoals (p : ProofSnapshot) : IO (List Format) :=
   Prod.fst <$> p.runMetaM do p.tacticState.goals.mapM (Meta.ppGoal ·)
+
 /--
 Construct a `ProofSnapshot` from a `ContextInfo` and optional `LocalContext`, and a list of goals.
-
 For convenience, we also allow a list of `Expr`s, and these are appended to the goals
 as fresh metavariables with the given types.
 -/
-def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Environment)
+def create (ctx : ContextInfo) (lctx? : Option LocalContext) (prevEnv? : Option Environment)
     (goals : List MVarId) (rootGoals? : Option (List MVarId)) (types : List Expr := [])
     : IO ProofSnapshot := do
-  ctx.runMetaM (lctx?.getD {}) do
-    let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t))
-    let s ← getThe Core.State
-    let s := match env? with
-    | none => s
-    | some env => { s with env }
-    pure <|
-    { coreState := s
-      coreContext := ← readThe Core.Context
-      metaState := ← getThe Meta.State
-      metaContext := ← readThe Meta.Context
-      termState := {}
-      termContext := {}
-      tacticState := { goals }
-      tacticContext := { elaborator := .anonymous }
-      rootGoals := match rootGoals? with
-        | none => goals
-        | some gs => gs }
+  -- Get the local context from the goals if not provided.
+  let lctx ← match lctx? with
+  | none => match goals with
+    | g :: _ => ctx.runMetaM {} do pure (← g.getDecl).lctx
+    | [] => match rootGoals? with
+      | some (g :: _) => ctx.runMetaM {} do pure (← g.getDecl).lctx
+      | _ => pure {}
+  | some lctx => pure lctx
+
+  ctx.runMetaM lctx do
+    -- update local instances, which is necessary when `types` is non-empty
+    Meta.withLocalInstances (lctx.decls.toList.filterMap id) do
+      let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t))
+      let s ← getThe Core.State
+      let s := match prevEnv? with
+      | none => s
+      | some env => { s with env }
+      pure <|
+      { coreState := s
+        coreContext := ← readThe Core.Context
+        metaState := ← getThe Meta.State
+        metaContext := ← readThe Meta.Context
+        termState := {}
+        termContext := {}
+        tacticState := { goals }
+        tacticContext := { elaborator := .anonymous }
+        rootGoals := match rootGoals? with
+          | none => goals
+          | some gs => gs }
 
 open Lean.Core in
 /-- A copy of `Core.State` with the `Environment`, caches, and logging omitted. -/
diff --git a/REPL/Util/Trie.lean b/REPL/Util/Trie.lean
new file mode 100644
index 00000000..bf095237
--- /dev/null
+++ b/REPL/Util/Trie.lean
@@ -0,0 +1,146 @@
+/-
+Utilities for working with Lean's string Trie without deep recursion.
+We provide iterative insert and matchPrefix to avoid stack overflows for
+very long strings (e.g., multi-KB inputs).
+-/
+
+import Lean.Data.Trie
+
+namespace REPL.Util.Trie
+
+open Lean
+open Lean.Data
+
+namespace Internal
+
+/-- Frames for rebuilding parent nodes after iteratively descending the trie. -/
+inductive Frame (α : Type) where
+  | node1 (v : Option α) (c : UInt8) : Frame α
+  | node (v : Option α) (cs : ByteArray) (ts : Array (Lean.Data.Trie α)) (idx : Nat) : Frame α
+  deriving Inhabited
+
+end Internal
+
+/-- Insert or replace the value at key `s` into trie `t` iteratively. -/
+def insert {α} (t : Lean.Data.Trie α) (s : String) (val : α) : Lean.Data.Trie α :=
+  Id.run do
+    let bytes := s.toUTF8
+    let n := bytes.size
+
+    -- Build the suffix path from position `start` to the end of `s`.
+    let mkSuffixFrom (start : Nat) : Lean.Data.Trie α :=
+      Id.run do
+        let mut r : Lean.Data.Trie α := Lean.Data.Trie.leaf (some val)
+        let mut j : Nat := n
+        while j > start do
+          let jp := j - 1
+          let c := bytes.get! jp
+          r := Lean.Data.Trie.node1 none c r
+          j := jp
+        return r
+
+    -- Descent state
+    let mut i : Nat := 0
+    let mut cur : Lean.Data.Trie α := t
+    let mut stack : Array (Internal.Frame α) := #[]
+
+    -- Iteratively descend until we either finish the key or need to branch/extend.
+    let mut done := false
+    let mut out := cur
+    while !done do
+      match cur with
+      | Lean.Data.Trie.leaf v =>
+        if i < n then
+          let c := bytes.get! i
+          let suffix := mkSuffixFrom (i + 1)
+          out := Lean.Data.Trie.node1 v c suffix
+        else
+          out := Lean.Data.Trie.leaf (some val)
+        done := true
+      | Lean.Data.Trie.node1 v c' t' =>
+        if i < n then
+          let c := bytes.get! i
+          if c == c' then
+            stack := stack.push (Internal.Frame.node1 v c')
+            cur := t'
+            i := i + 1
+          else
+            let suffix := mkSuffixFrom (i + 1)
+            out := Lean.Data.Trie.node v (ByteArray.mk #[c, c']) (#[(suffix), t'])
+            done := true
+        else
+          out := Lean.Data.Trie.node1 (some val) c' t'
+          done := true
+      | Lean.Data.Trie.node v cs ts =>
+        if i < n then
+          let c := bytes.get! i
+          match cs.findIdx? (· == c) with
+          | none =>
+            let suffix := mkSuffixFrom (i + 1)
+            out := Lean.Data.Trie.node v (cs.push c) (ts.push suffix)
+            done := true
+          | some idx =>
+            stack := stack.push (Internal.Frame.node v cs ts idx)
+            cur := ts[idx]!
+            i := i + 1
+        else
+          out := Lean.Data.Trie.node (some val) cs ts
+          done := true
+
+    -- Rebuild parents from the stack
+    let mut res := out
+    for frame in stack.reverse do
+      match frame with
+      | Internal.Frame.node1 v c =>
+        res := Lean.Data.Trie.node1 v c res
+      | Internal.Frame.node v cs ts idx =>
+        res := Lean.Data.Trie.node v cs (ts.set! idx res)
+    return res
+
+/--
+Find the longest key in the trie that is contained in the given string `s` at position `i`,
+and return the associated value, implemented iteratively to avoid stack overflows.
+
+Note the argument order is `(t s i)` to match usages in `Main.lean`.
+-/
+def matchPrefix {α} (t : Lean.Data.Trie α) (s : String) (i : String.Pos.Raw) : Option α :=
+  Id.run do
+    let bytes := s.toUTF8
+    let n := bytes.size
+    let mut idx : Nat := i.byteIdx
+    let mut cur : Lean.Data.Trie α := t
+    let mut best : Option α := none
+    let mut done := false
+    while !done do
+      match cur with
+      | Lean.Data.Trie.leaf v =>
+        if v.isSome then
+          return v
+        else
+          return best
+      | Lean.Data.Trie.node1 v c' t' =>
+        if v.isSome then best := v
+        if idx < n then
+          let c := bytes.get! idx
+          if c == c' then
+            idx := idx + 1
+            cur := t'
+          else
+            done := true
+        else
+          done := true
+      | Lean.Data.Trie.node v cs ts =>
+        if v.isSome then best := v
+        if idx < n then
+          let c := bytes.get! idx
+          match cs.findIdx? (· == c) with
+          | some j =>
+            idx := idx + 1
+            cur := ts[j]!
+          | none =>
+            done := true
+        else
+          done := true
+    return best
+
+end REPL.Util.Trie
diff --git a/test/Mathlib/test/incrementality.expected.out b/test/Mathlib/test/incrementality.expected.out
new file mode 100644
index 00000000..db70a9b3
--- /dev/null
+++ b/test/Mathlib/test/incrementality.expected.out
@@ -0,0 +1,70 @@
+{"tactics":
+ [{"usedConstants":
+   ["Nat.gcd",
+    "HMul.hMul",
+    "Mathlib.Meta.NormNum.isNat_eq_true",
+    "instMulNat",
+    "instOfNatNat",
+    "Mathlib.Meta.NormNum.isNat_ofNat",
+    "Tactic.NormNum.nat_gcd_helper_2",
+    "Nat.instAddMonoidWithOne",
+    "Nat",
+    "Eq.refl",
+    "Mathlib.Meta.NormNum.instAddMonoidWithOneNat",
+    "Tactic.NormNum.isNat_gcd",
+    "OfNat.ofNat",
+    "instHMul"],
+   "tactic": "norm_num",
+   "proofState": 0,
+   "pos": {"line": 2, "column": 60},
+   "goals": "⊢ Nat.gcd 180 168 = 12",
+   "endPos": {"line": 2, "column": 68}},
+  {"usedConstants": ["Eq.refl"],
+   "tactic": "rfl",
+   "proofState": 1,
+   "pos": {"line": 10, "column": 2},
+   "goals": "α✝ : Sort u_1\nn : α✝\n⊢ n = n",
+   "endPos": {"line": 10, "column": 5}}],
+ "messages":
+ [{"severity": "info",
+   "pos": {"line": 8, "column": 0},
+   "endPos": {"line": 8, "column": 5},
+   "data": "9227465"}],
+ "env": 0}
+
+{"tactics":
+ [{"usedConstants":
+   ["Nat.gcd",
+    "HMul.hMul",
+    "Mathlib.Meta.NormNum.isNat_eq_true",
+    "instMulNat",
+    "instOfNatNat",
+    "Mathlib.Meta.NormNum.isNat_ofNat",
+    "Tactic.NormNum.nat_gcd_helper_2",
+    "Nat.instAddMonoidWithOne",
+    "Nat",
+    "Eq.refl",
+    "Mathlib.Meta.NormNum.instAddMonoidWithOneNat",
+    "Tactic.NormNum.isNat_gcd",
+    "OfNat.ofNat",
+    "instHMul"],
+   "tactic": "norm_num",
+   "proofState": 2,
+   "pos": {"line": 2, "column": 60},
+   "goals": "⊢ Nat.gcd 180 168 = 12",
+   "endPos": {"line": 2, "column": 68}},
+  {"usedConstants": ["Nat", "Eq.refl"],
+   "tactic": "rfl",
+   "proofState": 3,
+   "pos": {"line": 10, "column": 2},
+   "goals": "n : ℕ\n⊢ n = n + 0",
+   "endPos": {"line": 10, "column": 5}}],
+ "messages":
+ [{"severity": "info",
+   "pos": {"line": 8, "column": 0},
+   "endPos": {"line": 8, "column": 5},
+   "data": "9227465"}],
+ "env": 1}
+
+{"env": 2}
+
diff --git a/test/Mathlib/test/incrementality.in b/test/Mathlib/test/incrementality.in
new file mode 100644
index 00000000..3e5c1738
--- /dev/null
+++ b/test/Mathlib/test/incrementality.in
@@ -0,0 +1,5 @@
+{"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n  | 0 => 0\n  | 1 => 1\n  | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo : n = n := by\n  rfl", "allTactics": true, "incrementality": true}
+
+{"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n  | 0 => 0\n  | 1 => 1\n  | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo2 : n = n+0 := by\n  rfl", "allTactics": true, "incrementality": true}
+
+{"cmd": "import Mathlib\n-- comment to test if header is reused even when a comment is added", "incrementality": true}
diff --git a/test/extract_declaration.expected.out b/test/extract_declaration.expected.out
new file mode 100644
index 00000000..965f3d37
--- /dev/null
+++ b/test/extract_declaration.expected.out
@@ -0,0 +1,806 @@
+{"env": 0,
+ "declarations":
+ [{"value":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 6, "column": 20},
+     "finish": {"line": 7, "column": 25}},
+    "pp": ":=\n  println \"Hello, world!\"",
+    "constants": ["println"]},
+   "type":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 6, "column": 12},
+     "finish": {"line": 6, "column": 19}},
+    "pp": "IO Unit",
+    "constants": ["IO", "Unit"]},
+   "signature":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 6, "column": 10},
+     "finish": {"line": 6, "column": 19}},
+    "pp": ": IO Unit",
+    "constants": ["IO", "Unit"]},
+   "scope":
+   {"varDecls": [],
+    "openDecl": [{"simple": {"namespace": "IO", "except": []}}],
+    "omitVars": [],
+    "levelNames": [],
+    "includeVars": [],
+    "currNamespace": "[anonymous]"},
+   "range":
+   {"synthetic": false,
+    "start": {"line": 6, "column": 0},
+    "finish": {"line": 7, "column": 25}},
+   "pp": "def hello : IO Unit :=\n  println \"Hello, world!\"",
+   "name": "hello",
+   "modifiers":
+   {"visibility": "regular",
+    "recKind": "default",
+    "isUnsafe": false,
+    "isProtected": false,
+    "docString": null,
+    "computeKind": "regular",
+    "attributes": []},
+   "kind": "definition",
+   "fullName": "hello",
+   "binders": null},
+  {"value":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 12, "column": 57},
+     "finish": {"line": 14, "column": 13}},
+    "pp": ":= by\n  intro h₁ h₂\n  rw [h₁, h₂]",
+    "constants": ["h₂", "h₁"]},
+   "type":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 12, "column": 35},
+     "finish": {"line": 12, "column": 56}},
+    "pp": "a = b → b = c → c = a",
+    "constants": ["c", "a", "b"]},
+   "signature":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 12, "column": 21},
+     "finish": {"line": 12, "column": 56}},
+    "pp": "{a b c : α} : a = b → b = c → c = a",
+    "constants": ["c", "α", "a", "b"]},
+   "scope":
+   {"varDecls": ["variable {α : Type u}"],
+    "openDecl": [],
+    "omitVars": [],
+    "levelNames": ["u"],
+    "includeVars": [],
+    "currNamespace": "[anonymous]"},
+   "range":
+   {"synthetic": false,
+    "start": {"line": 12, "column": 0},
+    "finish": {"line": 14, "column": 13}},
+   "pp":
+   "theorem eq_trans_sym {a b c : α} : a = b → b = c → c = a := by\n  intro h₁ h₂\n  rw [h₁, h₂]",
+   "name": "eq_trans_sym",
+   "modifiers":
+   {"visibility": "regular",
+    "recKind": "default",
+    "isUnsafe": false,
+    "isProtected": false,
+    "docString": null,
+    "computeKind": "regular",
+    "attributes": []},
+   "kind": "theorem",
+   "fullName": "eq_trans_sym",
+   "binders":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 12, "column": 21},
+     "finish": {"line": 12, "column": 32}},
+    "pp": "{a b c : α}",
+    "map":
+    [{"type": "α", "id": "a", "binderInfo": "implicit"},
+     {"type": "α", "id": "b", "binderInfo": "implicit"},
+     {"type": "α", "id": "c", "binderInfo": "implicit"}],
+    "groups": ["{a b c : α}"]}},
+  {"value":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 19, "column": 2},
+     "finish": {"line": 20, "column": 27}},
+    "pp": "| .zero => x\n  | .succ n => pow' x n * x",
+    "constants": ["pow'", "succ", "n", "x", "zero"]},
+   "type":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 18, "column": 27},
+     "finish": {"line": 18, "column": 34}},
+    "pp": "Nat → α",
+    "constants": ["α", "Nat"]},
+   "signature":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 18, "column": 9},
+     "finish": {"line": 18, "column": 34}},
+    "pp": "[Mul α] (x : α) : Nat → α",
+    "constants": ["α", "Mul", "Nat", "x"]},
+   "scope":
+   {"varDecls": ["variable {α : Type u}"],
+    "openDecl": [],
+    "omitVars": [],
+    "levelNames": ["u"],
+    "includeVars": [],
+    "currNamespace": "[anonymous]"},
+   "range":
+   {"synthetic": false,
+    "start": {"line": 16, "column": 0},
+    "finish": {"line": 20, "column": 27}},
+   "pp":
+   "/-- Docstring test\npow' x n = x ^ (n + 1) -/\ndef pow' [Mul α] (x : α) : Nat → α\n  | .zero => x\n  | .succ n => pow' x n * x",
+   "name": "pow'",
+   "modifiers":
+   {"visibility": "regular",
+    "recKind": "default",
+    "isUnsafe": false,
+    "isProtected": false,
+    "docString":
+    {"range":
+     {"synthetic": false,
+      "start": {"line": 16, "column": 0},
+      "finish": {"line": 17, "column": 25}},
+     "content": "/-- Docstring test\npow' x n = x ^ (n + 1) -/"},
+    "computeKind": "regular",
+    "attributes": []},
+   "kind": "definition",
+   "fullName": "pow'",
+   "binders":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 18, "column": 9},
+     "finish": {"line": 18, "column": 24}},
+    "pp": "[Mul α] (x : α)",
+    "map":
+    [{"type": "Mul α", "id": "", "binderInfo": "instImplicit"},
+     {"type": "α", "id": "x", "binderInfo": "default"}],
+    "groups": ["[Mul α]", "(x : α)"]}},
+  {"value": null,
+   "type":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 22, "column": 40},
+     "finish": {"line": 26, "column": 29}},
+    "pp":
+    "where\n  x : Nat\n  y : Nat\n  z : Nat\n  eqn : x ^ k + y ^ k = z ^ k",
+    "constants": ["eqn", "z", "y", "Nat", "k", "x"]},
+   "signature":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 22, "column": 23},
+     "finish": {"line": 26, "column": 29}},
+    "pp":
+    "(k : Nat) : Type where\n  x : Nat\n  y : Nat\n  z : Nat\n  eqn : x ^ k + y ^ k = z ^ k",
+    "constants": ["eqn", "z", "y", "Nat", "k", "x"]},
+   "scope":
+   {"varDecls": ["variable {α : Type u}"],
+    "openDecl": [],
+    "omitVars": [],
+    "levelNames": ["u"],
+    "includeVars": [],
+    "currNamespace": "[anonymous]"},
+   "range":
+   {"synthetic": false,
+    "start": {"line": 22, "column": 0},
+    "finish": {"line": 26, "column": 29}},
+   "pp":
+   "structure FermatTriple (k : Nat) : Type where\n  x : Nat\n  y : Nat\n  z : Nat\n  eqn : x ^ k + y ^ k = z ^ k",
+   "name": "FermatTriple",
+   "modifiers":
+   {"visibility": "regular",
+    "recKind": "default",
+    "isUnsafe": false,
+    "isProtected": false,
+    "docString": null,
+    "computeKind": "regular",
+    "attributes": []},
+   "kind": "structure",
+   "fullName": "FermatTriple",
+   "binders":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 22, "column": 23},
+     "finish": {"line": 22, "column": 39}},
+    "pp": "(k : Nat) : Type",
+    "map": [],
+    "groups": ["(k : Nat)", ": Type"]}},
+  {"value":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 28, "column": 25},
+     "finish": {"line": 28, "column": 44}},
+    "pp": ":= ⟨ 3, 4, 5, rfl ⟩",
+    "constants": ["rfl"]},
+   "type":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 28, "column": 10},
+     "finish": {"line": 28, "column": 24}},
+    "pp": "FermatTriple 2",
+    "constants": ["FermatTriple"]},
+   "signature":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 28, "column": 8},
+     "finish": {"line": 28, "column": 24}},
+    "pp": ": FermatTriple 2",
+    "constants": ["FermatTriple"]},
+   "scope":
+   {"varDecls": ["variable {α : Type u}"],
+    "openDecl": [],
+    "omitVars": [],
+    "levelNames": ["u"],
+    "includeVars": [],
+    "currNamespace": "[anonymous]"},
+   "range":
+   {"synthetic": false,
+    "start": {"line": 28, "column": 0},
+    "finish": {"line": 28, "column": 44}},
+   "pp": "example : FermatTriple 2 := ⟨ 3, 4, 5, rfl ⟩",
+   "name": "_example",
+   "modifiers":
+   {"visibility": "regular",
+    "recKind": "default",
+    "isUnsafe": false,
+    "isProtected": false,
+    "docString": null,
+    "computeKind": "regular",
+    "attributes": []},
+   "kind": "example",
+   "fullName": "_example",
+   "binders": null},
+  {"value":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 33, "column": 2},
+     "finish": {"line": 33, "column": 7}},
+    "pp": "| val",
+    "constants": ["val"]},
+   "type": null,
+   "signature":
+   {"range":
+    {"synthetic": true,
+     "start": {"line": 1, "column": 0},
+     "finish": {"line": 1, "column": 0}},
+    "pp": "",
+    "constants": []},
+   "scope":
+   {"varDecls": ["variable {α : Type u}"],
+    "openDecl": [],
+    "omitVars": [],
+    "levelNames": ["u"],
+    "includeVars": [],
+    "currNamespace": "Demo"},
+   "range":
+   {"synthetic": false,
+    "start": {"line": 32, "column": 0},
+    "finish": {"line": 33, "column": 7}},
+   "pp": "inductive MyType\n  | val",
+   "name": "MyType",
+   "modifiers":
+   {"visibility": "regular",
+    "recKind": "default",
+    "isUnsafe": false,
+    "isProtected": false,
+    "docString": null,
+    "computeKind": "regular",
+    "attributes": []},
+   "kind": "inductive",
+   "fullName": "Demo.MyType",
+   "binders": null},
+  {"value":
+   {"range":
+    {"synthetic": true,
+     "start": {"line": 35, "column": 0},
+     "finish": {"line": 35, "column": 32}},
+    "pp":
+    " :=  ParserDescr.trailingNode  `Demo.«term_≋_»  68  69  ParserDescr.binary  `andthen  ParserDescr.symbol  \" ≋ \"  ParserDescr.cat  `term  69 ",
+    "constants":
+    ["ParserDescr.binary._@.3937598925._hygCtx._hyg.4",
+     "ParserDescr.trailingNode._@.3937598925._hygCtx._hyg.4",
+     "ParserDescr.symbol._@.3937598925._hygCtx._hyg.4",
+     "ParserDescr.cat._@.3937598925._hygCtx._hyg.4"]},
+   "type":
+   {"range":
+    {"synthetic": true,
+     "start": {"line": 35, "column": 0},
+     "finish": {"line": 35, "column": 32}},
+    "pp": " Lean.TrailingParserDescr ",
+    "constants": ["Lean.TrailingParserDescr._@.3937598925._hygCtx._hyg.4"]},
+   "signature":
+   {"range":
+    {"synthetic": true,
+     "start": {"line": 35, "column": 0},
+     "finish": {"line": 35, "column": 32}},
+    "pp": " :  Lean.TrailingParserDescr ",
+    "constants": ["Lean.TrailingParserDescr._@.3937598925._hygCtx._hyg.4"]},
+   "scope":
+   {"varDecls": ["variable {α : Type u}"],
+    "openDecl": [],
+    "omitVars": [],
+    "levelNames": ["u"],
+    "includeVars": [],
+    "currNamespace": "Demo"},
+   "range":
+   {"synthetic": true,
+    "start": {"line": 35, "column": 0},
+    "finish": {"line": 35, "column": 32}},
+   "pp":
+   " @[ scoped  term_parser  1000  ]  public  meta  def  «term_≋_»  :  Lean.TrailingParserDescr  :=  ParserDescr.trailingNode  `Demo.«term_≋_»  68  69  ParserDescr.binary  `andthen  ParserDescr.symbol  \" ≋ \"  ParserDescr.cat  `term  69 ",
+   "name": "«term_≋_»",
+   "modifiers":
+   {"visibility": "public",
+    "recKind": "default",
+    "isUnsafe": false,
+    "isProtected": false,
+    "docString": null,
+    "computeKind": "meta",
+    "attributes": ["scoped  term_parser  1000"]},
+   "kind": "definition",
+   "fullName": "Demo.«term_≋_»",
+   "binders": null},
+  {"value":
+   {"range":
+    {"synthetic": true,
+     "start": {"line": 35, "column": 0},
+     "finish": {"line": 35, "column": 32}},
+    "pp":
+    " :=  fun  |  `(  $  lhs   ≋   $  rhs  )  =>  `  `( BEq.beq\n\n $  lhs  $  rhs  )  |  _  =>  no_error_if_unused%  throw  Lean.Macro.Exception.unsupportedSyntax ",
+    "constants":
+    ["throw._@.3937598925._hygCtx._hyg.9",
+     "lhs._@.3937598925._hygCtx._hyg.3",
+     "BEq.beq",
+     "rhs._@.3937598925._hygCtx._hyg.3",
+     "Lean.Macro.Exception.unsupportedSyntax._@.3937598925._hygCtx._hyg.9"]},
+   "type":
+   {"range":
+    {"synthetic": true,
+     "start": {"line": 35, "column": 0},
+     "finish": {"line": 35, "column": 32}},
+    "pp": " Macro ",
+    "constants": ["Macro._@.3937598925._hygCtx._hyg.9"]},
+   "signature":
+   {"range":
+    {"synthetic": true,
+     "start": {"line": 35, "column": 0},
+     "finish": {"line": 35, "column": 32}},
+    "pp": " :  Macro ",
+    "constants": ["Macro._@.3937598925._hygCtx._hyg.9"]},
+   "scope":
+   {"varDecls": ["variable {α : Type u}"],
+    "openDecl": [],
+    "omitVars": [],
+    "levelNames": ["u"],
+    "includeVars": [],
+    "currNamespace": "Demo"},
+   "range":
+   {"synthetic": true,
+    "start": {"line": 35, "column": 0},
+    "finish": {"line": 35, "column": 32}},
+   "pp":
+   " @[ scoped  macro  Demo.«term_≋_»  ]  public  meta  def  «_aux___macroRules_Demo_term_≋__1»  :  Macro  :=  fun  |  `(  $  lhs   ≋   $  rhs  )  =>  `  `( BEq.beq\n\n $  lhs  $  rhs  )  |  _  =>  no_error_if_unused%  throw  Lean.Macro.Exception.unsupportedSyntax ",
+   "name": "«_aux___macroRules_Demo_term_≋__1»",
+   "modifiers":
+   {"visibility": "public",
+    "recKind": "default",
+    "isUnsafe": false,
+    "isProtected": false,
+    "docString": null,
+    "computeKind": "meta",
+    "attributes": ["scoped  macro  Demo.«term_≋_»"]},
+   "kind": "definition",
+   "fullName": "Demo.«_aux___macroRules_Demo_term_≋__1»",
+   "binders": null},
+  {"value":
+   {"range":
+    {"synthetic": true,
+     "start": {"line": 35, "column": 0},
+     "finish": {"line": 35, "column": 32}},
+    "pp":
+    " :=  fun  |  `(  $  f  :  ident  $  lhs  $  rhs  )  =>  withRef  f  `(  $  lhs   ≋   $  rhs  )  |  _  =>  throw  (    ) ",
+    "constants":
+    ["throw._@.3937598925._hygCtx._hyg.4",
+     "f._@.3937598925._hygCtx._hyg.4",
+     "lhs._@.3937598925._hygCtx._hyg.3",
+     "_@.3937598925._hygCtx._hyg.4",
+     "rhs._@.3937598925._hygCtx._hyg.3",
+     "withRef._@.3937598925._hygCtx._hyg.4"]},
+   "type":
+   {"range":
+    {"synthetic": true,
+     "start": {"line": 35, "column": 0},
+     "finish": {"line": 35, "column": 32}},
+    "pp": " Lean.PrettyPrinter.Unexpander ",
+    "constants":
+    ["Lean.PrettyPrinter.Unexpander._@.3937598925._hygCtx._hyg.4"]},
+   "signature":
+   {"range":
+    {"synthetic": true,
+     "start": {"line": 35, "column": 0},
+     "finish": {"line": 35, "column": 32}},
+    "pp": " :  Lean.PrettyPrinter.Unexpander ",
+    "constants":
+    ["Lean.PrettyPrinter.Unexpander._@.3937598925._hygCtx._hyg.4"]},
+   "scope":
+   {"varDecls": ["variable {α : Type u}"],
+    "openDecl": [],
+    "omitVars": [],
+    "levelNames": ["u"],
+    "includeVars": [],
+    "currNamespace": "Demo"},
+   "range":
+   {"synthetic": true,
+    "start": {"line": 35, "column": 0},
+    "finish": {"line": 35, "column": 32}},
+   "pp":
+   " @[ scoped  app_unexpander  BEq.beq  ]  public  meta  def  _aux___unexpand_BEq_beq_1  :  Lean.PrettyPrinter.Unexpander  :=  fun  |  `(  $  f  :  ident  $  lhs  $  rhs  )  =>  withRef  f  `(  $  lhs   ≋   $  rhs  )  |  _  =>  throw  (    ) ",
+   "name": "_aux___unexpand_BEq_beq_1",
+   "modifiers":
+   {"visibility": "public",
+    "recKind": "default",
+    "isUnsafe": false,
+    "isProtected": false,
+    "docString": null,
+    "computeKind": "meta",
+    "attributes": ["scoped  app_unexpander  BEq.beq"]},
+   "kind": "definition",
+   "fullName": "Demo._aux___unexpand_BEq_beq_1",
+   "binders": null},
+  {"value":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 37, "column": 29},
+     "finish": {"line": 38, "column": 17}},
+    "pp": "where\n  beq _ _ := true",
+    "constants": ["beq", "true"]},
+   "type":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 37, "column": 18},
+     "finish": {"line": 37, "column": 28}},
+    "pp": "BEq MyType",
+    "constants": ["MyType", "BEq"]},
+   "signature":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 37, "column": 16},
+     "finish": {"line": 37, "column": 28}},
+    "pp": ": BEq MyType",
+    "constants": ["MyType", "BEq"]},
+   "scope":
+   {"varDecls": ["variable {α : Type u}"],
+    "openDecl": [],
+    "omitVars": [],
+    "levelNames": ["u"],
+    "includeVars": [],
+    "currNamespace": "Demo"},
+   "range":
+   {"synthetic": false,
+    "start": {"line": 37, "column": 0},
+    "finish": {"line": 38, "column": 17}},
+   "pp": "scoped instance : BEq MyType where\n  beq _ _ := true",
+   "name": "[anonymous]",
+   "modifiers":
+   {"visibility": "regular",
+    "recKind": "default",
+    "isUnsafe": false,
+    "isProtected": false,
+    "docString": null,
+    "computeKind": "regular",
+    "attributes": []},
+   "kind": "instance",
+   "fullName": "Demo.instBEqMyType",
+   "binders": null},
+  {"value":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 47, "column": 32},
+     "finish": {"line": 53, "column": 38}},
+    "pp":
+    ":= do\n  let x : Demo.MyType := Demo.MyType.val\n  let y : Demo.MyType := Demo.MyType.val\n  if x ≋ y then\n    IO.println \"x and y are equal\"\n  else\n    IO.println \"x and y are not equal\"",
+    "constants": ["IO.println", "Demo.MyType.val", "y", "Demo.MyType", "x"]},
+   "type":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 47, "column": 24},
+     "finish": {"line": 47, "column": 31}},
+    "pp": "IO Unit",
+    "constants": ["IO", "Unit"]},
+   "signature":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 47, "column": 22},
+     "finish": {"line": 47, "column": 31}},
+    "pp": ": IO Unit",
+    "constants": ["IO", "Unit"]},
+   "scope":
+   {"varDecls": ["variable {α : Type u}"],
+    "openDecl": [],
+    "omitVars": [],
+    "levelNames": ["u"],
+    "includeVars": [],
+    "currNamespace": "[anonymous]"},
+   "range":
+   {"synthetic": false,
+    "start": {"line": 47, "column": 0},
+    "finish": {"line": 53, "column": 38}},
+   "pp":
+   "def open_scoped_test1 : IO Unit := do\n  let x : Demo.MyType := Demo.MyType.val\n  let y : Demo.MyType := Demo.MyType.val\n  if x ≋ y then\n    IO.println \"x and y are equal\"\n  else\n    IO.println \"x and y are not equal\"",
+   "name": "open_scoped_test1",
+   "modifiers":
+   {"visibility": "regular",
+    "recKind": "default",
+    "isUnsafe": false,
+    "isProtected": false,
+    "docString": null,
+    "computeKind": "regular",
+    "attributes": []},
+   "kind": "definition",
+   "fullName": "open_scoped_test1",
+   "binders": null},
+  {"value":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 58, "column": 41},
+     "finish": {"line": 59, "column": 7}},
+    "pp": ":=\n  a * a",
+    "constants": ["a"]},
+   "type":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 58, "column": 37},
+     "finish": {"line": 58, "column": 40}},
+    "pp": "Nat",
+    "constants": ["Nat"]},
+   "signature":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 58, "column": 25},
+     "finish": {"line": 58, "column": 40}},
+    "pp": "(a : Nat) : Nat",
+    "constants": ["a", "Nat"]},
+   "scope":
+   {"varDecls": ["variable {α : Type u}"],
+    "openDecl": [],
+    "omitVars": [],
+    "levelNames": ["u"],
+    "includeVars": [],
+    "currNamespace": "[anonymous]"},
+   "range":
+   {"synthetic": false,
+    "start": {"line": 58, "column": 0},
+    "finish": {"line": 59, "column": 7}},
+   "pp": "private def private_test (a : Nat) : Nat :=\n  a * a",
+   "name": "private_test",
+   "modifiers":
+   {"visibility": "private",
+    "recKind": "default",
+    "isUnsafe": false,
+    "isProtected": false,
+    "docString": null,
+    "computeKind": "regular",
+    "attributes": []},
+   "kind": "definition",
+   "fullName": "_private.0.private_test",
+   "binders":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 58, "column": 25},
+     "finish": {"line": 58, "column": 34}},
+    "pp": "(a : Nat)",
+    "map": [{"type": "Nat", "id": "a", "binderInfo": "default"}],
+    "groups": ["(a : Nat)"]}},
+  {"value":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 61, "column": 62},
+     "finish": {"line": 61, "column": 66}},
+    "pp": ":= a",
+    "constants": ["a"]},
+   "type":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 61, "column": 58},
+     "finish": {"line": 61, "column": 61}},
+    "pp": "Nat",
+    "constants": ["Nat"]},
+   "signature":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 61, "column": 46},
+     "finish": {"line": 61, "column": 61}},
+    "pp": "(a : Nat) : Nat",
+    "constants": ["a", "Nat"]},
+   "scope":
+   {"varDecls": ["variable {α : Type u}"],
+    "openDecl": [],
+    "omitVars": [],
+    "levelNames": ["u"],
+    "includeVars": [],
+    "currNamespace": "[anonymous]"},
+   "range":
+   {"synthetic": false,
+    "start": {"line": 61, "column": 0},
+    "finish": {"line": 61, "column": 66}},
+   "pp": "private noncomputable def non_computable_test (a : Nat) : Nat := a",
+   "name": "non_computable_test",
+   "modifiers":
+   {"visibility": "private",
+    "recKind": "default",
+    "isUnsafe": false,
+    "isProtected": false,
+    "docString": null,
+    "computeKind": "noncomputable",
+    "attributes": []},
+   "kind": "definition",
+   "fullName": "_private.0.non_computable_test",
+   "binders":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 61, "column": 46},
+     "finish": {"line": 61, "column": 55}},
+    "pp": "(a : Nat)",
+    "map": [{"type": "Nat", "id": "a", "binderInfo": "default"}],
+    "groups": ["(a : Nat)"]}},
+  {"value":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 66, "column": 52},
+     "finish": {"line": 66, "column": 56}},
+    "pp": ":= a",
+    "constants": ["a"]},
+   "type":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 66, "column": 48},
+     "finish": {"line": 66, "column": 51}},
+    "pp": "Nat",
+    "constants": ["Nat"]},
+   "signature":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 66, "column": 36},
+     "finish": {"line": 66, "column": 51}},
+    "pp": "(a : Nat) : Nat",
+    "constants": ["a", "Nat"]},
+   "scope":
+   {"varDecls": ["variable {α : Type u}"],
+    "openDecl": [],
+    "omitVars": [],
+    "levelNames": ["u"],
+    "includeVars": [],
+    "currNamespace": "Example"},
+   "range":
+   {"synthetic": false,
+    "start": {"line": 64, "column": 0},
+    "finish": {"line": 66, "column": 56}},
+   "pp":
+   "/--\n dododo-/\nprotected partial def prot_part_def (a : Nat) : Nat := a",
+   "name": "prot_part_def",
+   "modifiers":
+   {"visibility": "regular",
+    "recKind": "partial",
+    "isUnsafe": false,
+    "isProtected": true,
+    "docString":
+    {"range":
+     {"synthetic": false,
+      "start": {"line": 64, "column": 0},
+      "finish": {"line": 65, "column": 9}},
+     "content": "/--\n dododo-/"},
+    "computeKind": "regular",
+    "attributes": []},
+   "kind": "definition",
+   "fullName": "Example.prot_part_def",
+   "binders":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 66, "column": 36},
+     "finish": {"line": 66, "column": 45}},
+    "pp": "(a : Nat)",
+    "map": [{"type": "Nat", "id": "a", "binderInfo": "default"}],
+    "groups": ["(a : Nat)"]}},
+  {"value":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 69, "column": 30},
+     "finish": {"line": 69, "column": 35}},
+    "pp": ":= 42",
+    "constants": []},
+   "type":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 69, "column": 26},
+     "finish": {"line": 69, "column": 29}},
+    "pp": "Nat",
+    "constants": ["Nat"]},
+   "signature":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 69, "column": 24},
+     "finish": {"line": 69, "column": 29}},
+    "pp": ": Nat",
+    "constants": ["Nat"]},
+   "scope":
+   {"varDecls": ["variable {α : Type u}"],
+    "openDecl": [],
+    "omitVars": [],
+    "levelNames": ["u"],
+    "includeVars": [],
+    "currNamespace": "[anonymous]"},
+   "range":
+   {"synthetic": false,
+    "start": {"line": 69, "column": 0},
+    "finish": {"line": 69, "column": 35}},
+   "pp": "@[simp, instance] def t : Nat := 42",
+   "name": "t",
+   "modifiers":
+   {"visibility": "regular",
+    "recKind": "default",
+    "isUnsafe": false,
+    "isProtected": false,
+    "docString": null,
+    "computeKind": "regular",
+    "attributes": ["simp", "instance"]},
+   "kind": "definition",
+   "fullName": "t",
+   "binders": null},
+  {"value":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 72, "column": 39},
+     "finish": {"line": 73, "column": 7}},
+    "pp": ":=\n  a + t",
+    "constants": ["t", "a"]},
+   "type":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 72, "column": 35},
+     "finish": {"line": 72, "column": 38}},
+    "pp": "Nat",
+    "constants": ["Nat"]},
+   "signature":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 72, "column": 23},
+     "finish": {"line": 72, "column": 38}},
+    "pp": "(a : Nat) : Nat",
+    "constants": ["a", "Nat"]},
+   "scope":
+   {"varDecls": ["variable {α : Type u}", "variable {β : Type u}"],
+    "openDecl": [],
+    "omitVars": [],
+    "levelNames": ["u"],
+    "includeVars": [],
+    "currNamespace": "[anonymous]"},
+   "range":
+   {"synthetic": false,
+    "start": {"line": 72, "column": 0},
+    "finish": {"line": 73, "column": 7}},
+   "pp": "public def public_test (a : Nat) : Nat :=\n  a + t",
+   "name": "public_test",
+   "modifiers":
+   {"visibility": "public",
+    "recKind": "default",
+    "isUnsafe": false,
+    "isProtected": false,
+    "docString": null,
+    "computeKind": "regular",
+    "attributes": []},
+   "kind": "definition",
+   "fullName": "public_test",
+   "binders":
+   {"range":
+    {"synthetic": false,
+     "start": {"line": 72, "column": 23},
+     "finish": {"line": 72, "column": 32}},
+    "pp": "(a : Nat)",
+    "map": [{"type": "Nat", "id": "a", "binderInfo": "default"}],
+    "groups": ["(a : Nat)"]}}]}
+
diff --git a/test/extract_declaration.in b/test/extract_declaration.in
new file mode 100644
index 00000000..ee592337
--- /dev/null
+++ b/test/extract_declaration.in
@@ -0,0 +1 @@
+{"path": "test/extract_declaration.lean", "declarations": true}
diff --git a/test/extract_declaration.lean b/test/extract_declaration.lean
new file mode 100644
index 00000000..586e1f74
--- /dev/null
+++ b/test/extract_declaration.lean
@@ -0,0 +1,73 @@
+import Lean
+
+/-! Inspired by Jixia examples -/
+
+open IO in
+def hello : IO Unit :=
+  println "Hello, world!"
+
+universe u
+variable {α : Type u}
+
+theorem eq_trans_sym {a b c : α} : a = b → b = c → c = a := by
+  intro h₁ h₂
+  rw [h₁, h₂]
+
+/-- Docstring test
+pow' x n = x ^ (n + 1) -/
+def pow' [Mul α] (x : α) : Nat → α
+  | .zero => x
+  | .succ n => pow' x n * x
+
+structure FermatTriple (k : Nat) : Type where
+  x : Nat
+  y : Nat
+  z : Nat
+  eqn : x ^ k + y ^ k = z ^ k
+
+example : FermatTriple 2 := ⟨ 3, 4, 5, rfl ⟩
+
+namespace Demo
+
+inductive MyType
+  | val
+
+scoped infix:68 " ≋ " => BEq.beq
+
+scoped instance : BEq MyType where
+  beq _ _ := true
+
+end Demo
+
+
+section
+
+open scoped Demo
+
+def open_scoped_test1 : IO Unit := do
+  let x : Demo.MyType := Demo.MyType.val
+  let y : Demo.MyType := Demo.MyType.val
+  if x ≋ y then
+    IO.println "x and y are equal"
+  else
+    IO.println "x and y are not equal"
+end
+
+section
+
+private def private_test (a : Nat) : Nat :=
+  a * a
+
+private noncomputable def non_computable_test (a : Nat) : Nat := a
+
+namespace Example
+/--
+ dododo-/
+protected partial def prot_part_def (a : Nat) : Nat := a
+end Example
+
+@[simp, instance] def t : Nat := 42
+
+variable {β : Type u}
+public def public_test (a : Nat) : Nat :=
+  a + t
diff --git a/test/in_command_dependency.expected.out b/test/in_command_dependency.expected.out
new file mode 100644
index 00000000..e22d70ba
--- /dev/null
+++ b/test/in_command_dependency.expected.out
@@ -0,0 +1,45 @@
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 21},
+   "goal": "⊢ False",
+   "endPos": {"line": 1, "column": 26}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"},
+  {"severity": "info",
+   "pos": {"line": 2, "column": 22},
+   "endPos": {"line": 2, "column": 28},
+   "data": "Try this:\n  [apply] exact x"}],
+ "env": 0}
+
+{"sorries":
+ [{"proofState": 1,
+   "pos": {"line": 1, "column": 21},
+   "goal": "⊢ False",
+   "endPos": {"line": 1, "column": 26}},
+  {"proofState": 2,
+   "pos": {"line": 2, "column": 19},
+   "goal": "⊢ False",
+   "endPos": {"line": 2, "column": 24}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"},
+  {"severity": "warning",
+   "pos": {"line": 2, "column": 0},
+   "endPos": {"line": 2, "column": 7},
+   "data": "declaration uses 'sorry'"}],
+ "env": 1}
+
+{"proofStatus": "Completed",
+ "proofState": 3,
+ "messages":
+ [{"severity": "info",
+   "pos": {"line": 0, "column": 0},
+   "endPos": {"line": 0, "column": 0},
+   "data": "Try this:\n  [apply] exact x"}],
+ "goals": []}
+
diff --git a/test/in_command_dependency.in b/test/in_command_dependency.in
new file mode 100644
index 00000000..78c0b6a9
--- /dev/null
+++ b/test/in_command_dependency.in
@@ -0,0 +1,6 @@
+{"cmd": "theorem x : False := sorry\nexample : False := by exact?"}
+
+{"cmd": "theorem x : False := sorry\nexample : False := sorry"}
+
+{"proofState": 2, "tactic": "exact?"}
+
diff --git a/test/local_instance_proof.expected.out b/test/local_instance_proof.expected.out
new file mode 100644
index 00000000..5a93d082
--- /dev/null
+++ b/test/local_instance_proof.expected.out
@@ -0,0 +1,62 @@
+{"env": 0}
+
+{"env": 1}
+
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 42},
+   "goal": "α : Type\ninst✝ : Inhabited α\n⊢ α",
+   "endPos": {"line": 1, "column": 47}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"}],
+ "env": 2}
+
+{"proofStatus": "Completed", "proofState": 1, "goals": []}
+
+{"sorries":
+ [{"proofState": 2,
+   "pos": {"line": 1, "column": 45},
+   "goal": "α : Type\ninst✝ : Inhabited α\n⊢ α",
+   "endPos": {"line": 1, "column": 50}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"}],
+ "env": 3}
+
+{"proofStatus": "Completed", "proofState": 3, "goals": []}
+
+{"env": 4}
+
+{"sorries":
+ [{"proofState": 4,
+   "pos": {"line": 1, "column": 17},
+   "goal": "α : Type\ns : Inhabited α\n⊢ α",
+   "endPos": {"line": 1, "column": 22}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"}],
+ "env": 5}
+
+{"proofStatus": "Completed", "proofState": 5, "goals": []}
+
+{"sorries":
+ [{"proofState": 6,
+   "pos": {"line": 1, "column": 20},
+   "goal": "α : Type\ns : Inhabited α\n⊢ α",
+   "endPos": {"line": 1, "column": 25}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"}],
+ "env": 6}
+
+{"proofStatus": "Completed", "proofState": 7, "goals": []}
+
diff --git a/test/local_instance_proof.in b/test/local_instance_proof.in
new file mode 100644
index 00000000..eeefd5ef
--- /dev/null
+++ b/test/local_instance_proof.in
@@ -0,0 +1,21 @@
+{"cmd": "def test (α : Type) [s : Inhabited α] : α := @Inhabited.default α s"}
+
+{"cmd": "def test2 (α : Type) [Inhabited α] : α := test α", "env": 0}
+
+{"cmd": "def test2 (α : Type) [Inhabited α] : α := sorry", "env": 0}
+
+{"tactic": "exact test α", "proofState": 0}
+
+{"cmd": "def test2 (α : Type) [Inhabited α] : α := by sorry", "env": 0}
+
+{"tactic": "exact test α", "proofState": 2}
+
+{"cmd": "variable (α : Type) [s : Inhabited α]", "env": 0}
+
+{"cmd": "def test2 : α := sorry", "env": 4}
+
+{"tactic": "exact test α", "proofState": 4}
+
+{"cmd": "def test2 : α := by sorry", "env": 4}
+
+{"tactic": "exact test α", "proofState": 6}