fix imports and tests

Author: kim-em

REPL/Frontend.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Lean.Elab.Frontend
-import REPL.Util.TermUnsafe
 
 open Lean Elab
 

REPL/Main.lean

@@ -6,7 +6,6 @@ Authors: Scott Morrison
 import REPL.JSON
 import REPL.Frontend
 import REPL.Util.Path
-import REPL.Util.TermUnsafe
 import REPL.Lean.ContextInfo
 import REPL.Lean.Environment
 import REPL.Lean.InfoTree

REPL/Snapshots.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Lean.Replay
+import Lean.Elab.Command
 import REPL.Util.Pickle
 
 open Lean Elab

REPL/Util/Pickle.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import REPL.Util.TermUnsafe
+import Lean.Environment
 
 /-!
 # Pickling and unpickling objects

REPL/Util/TermUnsafe.lean

@@ -12,14 +12,14 @@
 
 {"proofState": 1,
  "goals":
- ["case inl\nx : Int\nh : x < 0\n⊢ x = x",
-  "case inr\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
+ ["case pos\nx : Int\nh : x < 0\n⊢ x = x",
+  "case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
 
-{"proofState": 2, "goals": ["case inr\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
+{"proofState": 2, "goals": ["case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
 
 {"sorries":
- [{"proofState": 3, "goal": "case inl\nx : Int\nh : x < 0\n⊢ x = x"},
-  {"proofState": 4, "goal": "case inr\nx : Int\nh : ¬x < 0\n⊢ x = x"}],
+ [{"proofState": 3, "goal": "case pos\nx : Int\nh : x < 0\n⊢ x = x"},
+  {"proofState": 4, "goal": "case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"}],
  "proofState": 5,
  "goals": []}
 

test/by_cases.expected.out

@@ -2,7 +2,7 @@
 
 {"proofState" : 0, "tactic": "by_cases h : x < 0"}
 
-{"proofState" : 1, "tactic": "case inl => rfl"}
+{"proofState" : 1, "tactic": "case pos => rfl"}
 
 {"proofState" : 1, "tactic": "all_goals sorry"}
 

test/by_cases.in

@@ -23,11 +23,15 @@
  "proofState": 5,
  "goals": []}
 
-{"traces": ["[Meta.Tactic.simp.rewrite] h0:1000, x > 0 ==> True"],
+{"traces":
+ ["[Meta.Tactic.simp.rewrite] @gt_iff_lt:1000, x > 0 ==> 0 < x",
+  "[Meta.Tactic.simp.rewrite] h0:1000, 0 < x ==> True"],
  "proofState": 6,
  "goals": []}
 
-{"traces": ["[Meta.Tactic.simp.rewrite] h0:1000, x > 0 ==> True"],
+{"traces":
+ ["[Meta.Tactic.simp.rewrite] @gt_iff_lt:1000, x > 0 ==> 0 < x",
+  "[Meta.Tactic.simp.rewrite] h0:1000, 0 < x ==> True"],
  "proofState": 7,
  "goals": []}