max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test(tests/lean/interactive): add regression test for #1313

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-20 21:48:19 -08:00
parent e2bf4fcddb
commit 9c9cad6ae8
2 changed files with 45 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
tests/lean/interactive/1313.lean Normal file
View file

@ -0,0 +1,34 @@
example (p q : Prop) (a : p) (b : q) : p ∧ q ∧ p :=
begin
--^ "command": "info"
end
example (p q : Prop) (a : p) (b : q) : p ∧ q ∧ p :=
begin
apply and.intro,
--^ "command": "info"
end
example (p q : Prop) (a : p) (b : q) : p ∧ q ∧ p :=
begin
apply and.intro,
--^ "command": "info"
end
example (p q : Prop) (a : p) (b : q) : p ∧ q ∧ p :=
begin
apply and.intro,
--^ "command": "info"
end
example (p q : Prop) (a : p) (b : q) : p ∧ q ∧ p :=
begin
apply and.intro,
--^ "command": "info"
{exact a},
end

11
tests/lean/interactive/1313.lean.expected.out Normal file
View file

@ -0,0 +1,11 @@
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":5,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p ∧ q ∧ p"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":12,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":18,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":25,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":34,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"additional_message"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"state":"p q : Prop,\na : p,\nb : q\n⊢ p ∧ q ∧ p"},"response":"ok","seq_num":4}
{"record":{"state":"p q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"ok","seq_num":11}
{"record":{"state":"p q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"ok","seq_num":17}
{"record":{"state":"p q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"ok","seq_num":24}
{"record":{"state":"p q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"ok","seq_num":32}