diff --git a/docs/drafting.ipynb b/docs/drafting.ipynb
index f5dfd5a..59011cf 100644
--- a/docs/drafting.ipynb
+++ b/docs/drafting.ipynb
@@ -10,7 +10,7 @@
     "Pantograph supports drafting (technically the sketch step) from\n",
     "[Draft-Sketch-Prove](https://github.com/wellecks/ntptutorial/tree/main/partII_dsp).\n",
     "Pantograph's drafting feature is more powerful. At any place in the proof, you\n",
-    "can replace an expression with `sorry`, and the `sorry` will become a goal.\n",
+    "can replace an expression with `sorry`, and the `sorry` will become a goal. Any type errors will also become goals. In order to detect whether type errors have occurred, the user can look at the messages from each compilation unit.\n",
     "\n",
     "At this point we must introduce the idea of compilation units. Each Lean\n",
     "definition, theorem, constant, etc., is a *compilation unit*. When Pantograph\n",
@@ -120,8 +120,8 @@
     "\"\"\"\n",
     "\n",
     "server = Server()\n",
-    "state0, = server.load_sorry(sketch)\n",
-    "print(state0)"
+    "unit, = server.load_sorry(sketch)\n",
+    "print(unit.goal_state)"
    ]
   },
   {
@@ -157,7 +157,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.12.6"
+   "version": "3.12.7"
   }
  },
  "nbformat": 4,
diff --git a/examples/all.ipynb b/examples/all.ipynb
deleted file mode 100644
index 121cd5a..0000000
--- a/examples/all.ipynb
+++ /dev/null
@@ -1,448 +0,0 @@
-{
- "cells": [
-  {
-   "cell_type": "markdown",
-   "id": "a1078f98-fcaf-4cda-8ad4-3cbab44f114b",
-   "metadata": {},
-   "source": [
-    "# Pantograph Example\n",
-    "\n",
-    "The only interface for interacting with Pantograph is the `Server` class. It can be used either standalone (with no Lean project specified) or in a Lean project in order to access the project's symbols (e.g. Mathlib).\n",
-    "\n",
-    "The server's `imports` argument must be specified as a list of Lean modules to import. With no import statements, there are no symbols available and no useful work can be done. By default, `imports` is `[\"Init\"]`."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 1,
-   "id": "101f4591-ec31-4000-96a6-ac3fc3dd0fa2",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "from pantograph import Server\n",
-    "\n",
-    "server = Server()"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "1fbdb837-740e-44ef-a7e9-c40f79584639",
-   "metadata": {},
-   "source": [
-    "We can initialize a proof by providing the target statement."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 2,
-   "id": "4affc375-360b-40cf-8d22-4fdcc12dba0d",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "state0 = server.goal_start(\"forall (p : Prop), p -> p\")"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "deb7994a-273f-4b52-be2d-e1086d4c1d55",
-   "metadata": {},
-   "source": [
-    "This invocation creates a *goal state*, which consists of a finite number of goals. "
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 3,
-   "id": "29f7ae15-7f69-4740-a6fa-71fbb1ccabd8",
-   "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/plain": [
-       "GoalState(state_id=0, goals=[Goal(variables=[], target='forall (p : Prop), p -> p', name=None, is_conversion=False)], _sentinel=[])"
-      ]
-     },
-     "execution_count": 3,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
-   "source": [
-    "state0"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "274f50da-85c1-445e-bf9f-cb716f66e36f",
-   "metadata": {},
-   "source": [
-    "Execute tactics on the goal state via `Server.goal_tactic`:"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 4,
-   "id": "bfbd5512-fcb0-428d-8131-4da4005e743c",
-   "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/plain": [
-       "GoalState(state_id=1, goals=[Goal(variables=[Variable(t='Prop', v=None, name='p✝')], target='p✝ → p✝', name=None, is_conversion=False)], _sentinel=[])"
-      ]
-     },
-     "execution_count": 4,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
-   "source": [
-    "state1 = server.goal_tactic(state0, goal_id=0, tactic=\"intro\")\n",
-    "state1"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "1c1c5ab4-5518-40b0-8a2f-50e095a3702a",
-   "metadata": {},
-   "source": [
-    "Recover the usual string form of a goal by the `str` function:"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 5,
-   "id": "2d18d6dc-7936-4bb6-b47d-f781dd8ddacd",
-   "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/plain": [
-       "'p✝ : Prop\\n⊢ p✝ → p✝'"
-      ]
-     },
-     "execution_count": 5,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
-   "source": [
-    "str(state1.goals[0])"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "fc560b88-0222-4e40-bff9-37ab70af075e",
-   "metadata": {},
-   "source": [
-    "When a tactic fails, it throws an exception:"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 6,
-   "id": "a0fdd3b3-9b38-4602-84a3-89065822f6e8",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "[\"tactic 'assumption' failed\\np✝ : Prop\\n⊢ p✝ → p✝\"]\n"
-     ]
-    }
-   ],
-   "source": [
-    "try:\n",
-    "    state2 = server.goal_tactic(state1, goal_id=0, tactic=\"assumption\")\n",
-    "    print(\"Should not reach this\")\n",
-    "except Exception as e:\n",
-    "    print(e)"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "c801bbb4-9248-4f75-945b-1dd665bb08d1",
-   "metadata": {},
-   "source": [
-    "A state with no goals is considered solved"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 7,
-   "id": "9d18045a-9734-415c-8f40-7aadb6cb18f4",
-   "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/plain": [
-       "GoalState(state_id=3, goals=[], _sentinel=[])"
-      ]
-     },
-     "execution_count": 7,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
-   "source": [
-    "state2 = server.goal_tactic(state1, goal_id=0, tactic=\"intro h\")\n",
-    "state3 = server.goal_tactic(state2, goal_id=0, tactic=\"exact h\")\n",
-    "state3"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "aa5a2800-cae3-48df-b746-d19a8d84eaf5",
-   "metadata": {},
-   "source": [
-    "Execute `Server.gc()` to clean up unused goals once in a while"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 8,
-   "id": "ee98de99-3cfc-4449-8d62-00e8eaee03db",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "server.gc()"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "78cfb9ac-c5ec-4901-97a5-4d19e6b8ecbb",
-   "metadata": {},
-   "source": [
-    "## Loading Projects\n",
-    "\n",
-    "Pantograph would not be useful if it could not load symbols from other projects. In `examples/Example` is a standard Lean 4 project, with its toolchain version precisely equal to the toolchain version of Pantograph. Executing `lake new PROJECT_NAME` or `lake init` in an empty folder initializes a project according to this specification. To use a project in Pantograph, compile the project by running `lake build` in its root directory. This sets up output folders and builds the binary Lean files.\n",
-    "\n",
-    "Load the example project by providing `project_path` and `lean_path` to `Server`:"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 9,
-   "id": "ecf5d9d3-e53e-4f67-969e-d38e3d97c65e",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "$PWD: /home/aniva/Projects/atp/PyPantograph/examples/Example\n",
-      "$LEAN_PATH: b'././.lake/packages/batteries/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/build/lib:/home/aniva/.elan/toolchains/leanprover--lean4---v4.12/lib/lean\\n'\n"
-     ]
-    }
-   ],
-   "source": [
-    "import subprocess, os\n",
-    "from pathlib import Path\n",
-    "project_path = Path(os.getcwd()).resolve() / 'Example'\n",
-    "print(f\"$PWD: {project_path}\")\n",
-    "server = Server(imports=['Example'], project_path=project_path)"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "67123741-3d23-4077-98ab-91110b4e39f1",
-   "metadata": {},
-   "source": [
-    "With the project loaded, all dependencies of the project, be it Mathlib or Aesop, are now available."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 10,
-   "id": "bf485778-baa9-4c1c-80fa-960f9cf9bc8a",
-   "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/plain": [
-       "True"
-      ]
-     },
-     "execution_count": 10,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
-   "source": [
-    "state0 = server.goal_start(\"forall (p q: Prop), Or p q -> Or q p\")\n",
-    "state1 = server.goal_tactic(state0, goal_id=0, tactic=\"aesop\")\n",
-    "state1.is_solved"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "8c3f9d90-bacc-4cba-95a4-23cc31a58a4f",
-   "metadata": {},
-   "source": [
-    "## Reading Symbols\n",
-    "\n",
-    "Pantograph can also query proof states from a project by directly calling into Lean's compiler internals. Run the Lean compiler on a Lean file via `Server.tactic_invocations`. Feeding in the absolute path is preferred."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 11,
-   "id": "8ff6007b-50df-4449-9a86-6d3eb0bc0caa",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "==== #0 ====\n",
-      "/-- Ensure that Aesop is running -/\n",
-      "example : α → α :=\n",
-      "  by aesop\n",
-      "\n",
-      "\n",
-      "==== #1 ====\n",
-      "example : ∀ (p q: Prop), p ∨ q → q ∨ p := by\n",
-      "  intro p q h\n",
-      "  -- Here are some comments\n",
-      "  cases h\n",
-      "  . apply Or.inr\n",
-      "    assumption\n",
-      "  . apply Or.inl\n",
-      "    assumption\n",
-      "\n",
-      "==== Invocations ====\n",
-      "α : Sort ?u.7\n",
-      "⊢ α → α\n",
-      "aesop\n",
-      "\n",
-      "\n",
-      "⊢ ∀ (p q : Prop), p ∨ q → q ∨ p\n",
-      "intro p q h\n",
-      "p q : Prop\n",
-      "h : p ∨ q\n",
-      "⊢ q ∨ p\n",
-      "\n",
-      "p q : Prop\n",
-      "h : p ∨ q\n",
-      "⊢ q ∨ p\n",
-      "cases h\n",
-      "case inl\n",
-      "p q : Prop\n",
-      "h✝ : p\n",
-      "⊢ q ∨ p\n",
-      "case inr p q : Prop h✝ : q ⊢ q ∨ p\n",
-      "\n",
-      "case inl\n",
-      "p q : Prop\n",
-      "h✝ : p\n",
-      "⊢ q ∨ p\n",
-      "apply Or.inr\n",
-      "case inl.h\n",
-      "p q : Prop\n",
-      "h✝ : p\n",
-      "⊢ p\n",
-      "\n",
-      "case inl.h\n",
-      "p q : Prop\n",
-      "h✝ : p\n",
-      "⊢ p\n",
-      "assumption\n",
-      "\n",
-      "\n",
-      "case inr\n",
-      "p q : Prop\n",
-      "h✝ : q\n",
-      "⊢ q ∨ p\n",
-      "apply Or.inl\n",
-      "case inr.h\n",
-      "p q : Prop\n",
-      "h✝ : q\n",
-      "⊢ q\n",
-      "\n",
-      "case inr.h\n",
-      "p q : Prop\n",
-      "h✝ : q\n",
-      "⊢ q\n",
-      "assumption\n",
-      "\n",
-      "\n"
-     ]
-    }
-   ],
-   "source": [
-    "units, invocations = server.tactic_invocations(project_path / \"Example.lean\")\n",
-    "for i, u in enumerate(units):\n",
-    "    print(f\"==== #{i} ====\")\n",
-    "    print(u)\n",
-    "print(\"==== Invocations ====\")\n",
-    "for i in invocations:\n",
-    "    print(f\"{i.before}\\n{i.tactic}\\n{i.after}\\n\")"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "8762b719-d13b-4714-84ff-48c44b18f364",
-   "metadata": {},
-   "source": [
-    "### Loading a theorem for the agent to prove\n",
-    "\n",
-    "For this to work, write `sorry` in the place where you would like your agent to do work, for example\n",
-    "```lean\n",
-    "example : (p q: Prop): Or p q -> Or q p := sorry\n",
-    "```\n",
-    "Then use the `Server.load_sorry`. As long as you only have one statement in `command`, it will give you exactly one goal state. A command with no `sorry`s results in no goal states.\n",
-    "\n",
-    "Note: Since a syntactically incorrect command will not generate `sorry`s, they will be sliently ignored by the frontend. Check if this is the case if the function returns no goals."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 12,
-   "id": "3c515d2b-6910-499e-953b-bc69dc0e0a57",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "GoalState(state_id=2, goals=[Goal(variables=[Variable(t='Prop', v=None, name='p'), Variable(t='Prop', v=None, name='q')], target='p ∨ q → q ∨ p', name=None, is_conversion=False)], _sentinel=[0])\n"
-     ]
-    }
-   ],
-   "source": [
-    "state0, = server.load_sorry(\"example (p q: Prop): Or p q -> Or q p := sorry\")\n",
-    "print(state0)"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "id": "50b90547-fcbf-419f-866e-a6ebcc925c5f",
-   "metadata": {},
-   "outputs": [],
-   "source": []
-  }
- ],
- "metadata": {
-  "kernelspec": {
-   "display_name": "Python 3 (ipykernel)",
-   "language": "python",
-   "name": "python3"
-  },
-  "language_info": {
-   "codemirror_mode": {
-    "name": "ipython",
-    "version": 3
-   },
-   "file_extension": ".py",
-   "mimetype": "text/x-python",
-   "name": "python",
-   "nbconvert_exporter": "python",
-   "pygments_lexer": "ipython3",
-   "version": "3.12.6"
-  }
- },
- "nbformat": 4,
- "nbformat_minor": 5
-}