diff --git a/test/all_tactics.expected.out b/test/all_tactics.expected.out new file mode 100644 index 0000000..7659683 --- /dev/null +++ b/test/all_tactics.expected.out @@ -0,0 +1,13 @@ +{"tactics": + [{"tactic": "have t := 37", + "proofState": 0, + "pos": {"line": 1, "column": 18}, + "goals": "⊢ Nat", + "endPos": {"line": 1, "column": 30}}, + {"tactic": "exact t", + "proofState": 1, + "pos": {"line": 1, "column": 32}, + "goals": "t : Nat ⊢ Nat", + "endPos": {"line": 1, "column": 39}}], + "env": 0} + diff --git a/test/all_tactics.in b/test/all_tactics.in new file mode 100644 index 0000000..5736d87 --- /dev/null +++ b/test/all_tactics.in @@ -0,0 +1 @@ +{"cmd": "def f : Nat := by have t := 37; exact t", "allTactics": true} diff --git a/test/calc.expected.out b/test/calc.expected.out new file mode 100644 index 0000000..8660a00 --- /dev/null +++ b/test/calc.expected.out @@ -0,0 +1,32 @@ +{"tactics": + [{"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}}, + {"tactic": "sorry", + "proofState": 3, + "pos": {"line": 2, "column": 14}, + "goals": "⊢ 3 = 4", + "endPos": {"line": 2, "column": 19}}, + {"tactic": "sorry", + "proofState": 4, + "pos": {"line": 3, "column": 14}, + "goals": "⊢ 4 = 5", + "endPos": {"line": 3, "column": 19}}], + "sorries": + [{"proofState": 0, + "pos": {"line": 2, "column": 14}, + "goal": "⊢ 3 = 4", + "endPos": {"line": 2, "column": 19}}, + {"proofState": 1, + "pos": {"line": 3, "column": 14}, + "goal": "⊢ 4 = 5", + "endPos": {"line": 3, "column": 19}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 0}, + "endPos": {"line": 1, "column": 7}, + "data": "declaration uses 'sorry'"}], + "env": 0} + diff --git a/test/calc.in b/test/calc.in new file mode 100644 index 0000000..895da44 --- /dev/null +++ b/test/calc.in @@ -0,0 +1 @@ +{"cmd": "example : 3 = 5 := by calc\n 3 = 4 := by sorry\n 4 = 5 := by sorry", "allTactics": true }