update calc.expected.out

leanprover-community · Nov 4, 2024 · 54ee057 · 54ee057
1 parent c2fae54
commit 54ee057
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 4 deletions.
diff --git 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
@@ -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}}],