Add test

Author: augustepoiroux

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": []}
+

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}