Skip to content

Commit de07032

Browse files
Update readme
1 parent 6c4f87a commit de07032

File tree

3 files changed

+9
-3
lines changed

3 files changed

+9
-3
lines changed

README.md

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,8 @@ Example output:
4444
{"sorries":
4545
[{"pos": {"line": 1, "column": 18},
4646
"endPos": {"line": 1, "column": 23},
47-
"goal": "⊢ Nat",
47+
"parentDecl": "h",
48+
"goals": ["⊢ Nat"],
4849
"proofState": 0}],
4950
"messages":
5051
[{"severity": "error",
@@ -92,12 +93,13 @@ and then use the `proofState` index returned for each `sorry`.
9293

9394
Example usage:
9495
```json
95-
{"cmd" : "def f (x : Unit) : Nat := by sorry"}
96+
{"cmd" : "def f (x : Unit) : Nat := by sorry", "sorries": "individual"}
9697

9798
{"sorries":
9899
[{"proofState": 0,
99100
"pos": {"line": 1, "column": 29},
100-
"goal": "x : Unit\n⊢ Nat",
101+
"parentDecl": "f",
102+
"goals": ["x : Unit\n⊢ Nat"],
101103
"endPos": {"line": 1, "column": 34}}],
102104
"messages":
103105
[{"severity": "warning",

test/sketch_file.expected.out

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,3 +47,5 @@
4747

4848
{"proofStatus": "Completed", "proofState": 5, "goals": []}
4949

50+
{"proofStatus": "Completed", "proofState": 6, "goals": []}
51+

test/sketch_file.in

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,3 +7,5 @@
77
{"tactic": "rw [Nat.succ_add, Nat.add_succ, ih]", "proofState": 3}
88

99
{"tactic": "apply Nat.add_zero", "proofState": 4}
10+
11+
{"tactic": "(\nintros; rfl)", "proofState": 1}

0 commit comments

Comments
 (0)