From 54ee057282177e898e971b43ae58af564fecf11d Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 4 Nov 2024 18:51:11 +1100
Subject: [PATCH] update calc.expected.out

---
 REPL/Snapshots.lean    |  1 -
 test/calc.expected.out | 19 ++++++++++++++++---
 2 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean
index 2e3e71f..1114c24 100644
--- a/REPL/Snapshots.lean
+++ b/REPL/Snapshots.lean
@@ -194,7 +194,6 @@ def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Envi
     (goals : 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))
-    goals.head!.withContext do
     let s ← getThe Core.State
     let s := match env? with
     | none => s
diff --git a/test/calc.expected.out b/test/calc.expected.out
index fde8fee..94f6a9f 100644
--- a/test/calc.expected.out
+++ b/test/calc.expected.out
@@ -1,22 +1,35 @@
 {"tactics":
  [{"usedConstants":
-   ["Trans.trans", "instOfNatNat", "instTransEq", "Nat", "OfNat.ofNat", "Eq"],
+   ["Trans.trans",
+    "sorryAx",
+    "instOfNatNat",
+    "instTransEq",
+    "Nat",
+    "OfNat.ofNat",
+    "Bool.false",
+    "Eq"],
    "tactic": "calc\n  3 = 4 := by sorry\n  4 = 5 := by sorry",
    "proofState": 2,
    "pos": {"line": 1, "column": 22},
    "goals": "⊢ 3 = 5",
    "endPos": {"line": 3, "column": 19}},
+  {"usedConstants": [],
+   "tactic": "\n  3 = 4 := by sorry\n  4 = 5 := by sorry",
+   "proofState": 3,
+   "pos": {"line": 2, "column": 2},
+   "goals": "no goals",
+   "endPos": {"line": 3, "column": 19}},
   {"usedConstants":
    ["sorryAx", "instOfNatNat", "Nat", "OfNat.ofNat", "Bool.false", "Eq"],
    "tactic": "sorry",
-   "proofState": 3,
+   "proofState": 4,
    "pos": {"line": 2, "column": 14},
    "goals": "⊢ 3 = 4",
    "endPos": {"line": 2, "column": 19}},
   {"usedConstants":
    ["sorryAx", "instOfNatNat", "Nat", "OfNat.ofNat", "Bool.false", "Eq"],
    "tactic": "sorry",
-   "proofState": 4,
+   "proofState": 5,
    "pos": {"line": 3, "column": 14},
    "goals": "⊢ 4 = 5",
    "endPos": {"line": 3, "column": 19}}],