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

chore(tests/lean/interactive): fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2017-06-15 10:56:09 -07:00
parent bf0d785888
commit fe774a25cf
5 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/interactive/complete.lean.expected.out
View file

@ -1,4 +1,4 @@
{"msgs":[{"caption":"print result","file_name":"f","pos_col":0,"pos_line":19,"severity":"information","text":"inductive foo : Type\nconstructors:"}],"response":"all_messages"}
{"msgs":[{"caption":"print result","end_pos_col":0,"end_pos_line":22,"file_name":"f","pos_col":0,"pos_line":19,"severity":"information","text":"inductive foo : Type\nconstructors:"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"completions":[{"source":,"text":"foo","type":"Type"},{"source":{"column":10,"line":3},"text":"foo.rec","type":"Π (C : foo → Sort l) (n : foo), C n"},{"source":{"column":10,"line":3},"text":"foo.rec_on","type":"Π (C : foo → Sort l) (n : foo), C n"}],"prefix":"fo","response":"ok","seq_num":6}
{"response":"ok","seq_num":10}

2
tests/lean/interactive/hole4.lean.expected.out
View file

@ -1,3 +1,3 @@
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"warning","text":"declaration 'x' uses sorry"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"replacements":{"alternatives":[{"code":"λ (a : ℕ), {! !}","description":""}],"end":{"column":16,"line":2},"file":"f","start":{"column":0,"line":2}},"response":"ok","seq_num":3}
{"replacements":{"alternatives":[{"code":"λ (a : ℕ), {! !}","description":""}],"end":{"column":12,"line":2},"file":"f","start":{"column":0,"line":2}},"response":"ok","seq_num":3}

2
tests/lean/interactive/info.lean.expected.out
View file

@ -1,4 +1,4 @@
{"msgs":[{"caption":"print result","file_name":"f","pos_col":0,"pos_line":18,"severity":"information","text":"@[inline]\ndef id : Π {α : Sort u}, α → α :=\nλ {α : Sort u} (a : α), a"}],"response":"all_messages"}
{"msgs":[{"caption":"print result","end_pos_col":26,"end_pos_line":19,"file_name":"f","pos_col":0,"pos_line":18,"severity":"information","text":"@[inline]\ndef id : Π {α : Sort u}, α → α :=\nλ {α : Sort u} (a : α), a"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"source":},"response":"ok","seq_num":2}
{"record":{"doc":"reducible"},"response":"ok","seq_num":5}

2
tests/lean/interactive/info_id_pre_elab.lean.expected.out
View file

@ -1,7 +1,7 @@
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"f","pos_col":8,"pos_line":3,"severity":"error","text":"ambiguous overload, possible interpretations\n trace\n tactic.trace\nAdditional information:\nf:3:8: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"f","pos_col":8,"pos_line":3,"severity":"error","text":"ambiguous overload, possible interpretations\n trace\n tactic.trace\nAdditional information:\nf:3:8: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available"},{"caption":"","file_name":"f","pos_col":27,"pos_line":7,"severity":"error","text":"invalid expression, `)` expected"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"f","pos_col":8,"pos_line":3,"severity":"error","text":"ambiguous overload, possible interpretations\n trace\n tactic.trace\nAdditional information:\nf:3:8: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available"},{"caption":"","file_name":"f","pos_col":27,"pos_line":7,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"check result","file_name":"f","pos_col":0,"pos_line":6,"severity":"information","text":"λ (tac : tactic unit), (abstract tac none) : tactic unit → tactic unit"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"f","pos_col":8,"pos_line":3,"severity":"error","text":"ambiguous overload, possible interpretations\n trace\n tactic.trace\nAdditional information:\nf:3:8: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available"},{"caption":"","file_name":"f","pos_col":27,"pos_line":7,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"check result","end_pos_col":27,"end_pos_line":7,"file_name":"f","pos_col":0,"pos_line":6,"severity":"information","text":"λ (tac : tactic unit), (abstract tac none) : tactic unit → tactic unit"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"response":"ok","seq_num":4}
{"record":{"full-id":"tactic.abstract","source":,"type":"tactic unit → opt_param (option name) none → opt_param bool tt → tactic unit"},"response":"ok","seq_num":7}

6
tests/lean/interactive/rb_map_ts.lean.expected.out
View file

@ -1,7 +1,7 @@
{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"}],"response":"all_messages"}
{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"}],"response":"all_messages"}
{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":81,"severity":"information","text":"test\n"}],"response":"all_messages"}
{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":81,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":89,"severity":"information","text":"theorem ex₂ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"}],"response":"all_messages"}
{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":77,"file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"}],"response":"all_messages"}
{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":77,"file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":81,"severity":"information","text":"test\n"}],"response":"all_messages"}
{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":77,"file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":81,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":10,"end_pos_line":89,"file_name":"f","pos_col":0,"pos_line":89,"severity":"information","text":"theorem ex₂ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"source":,"state":"Custom state: ⟨x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p ∧ q","tactic_params":["(string)"],"text":"trace","type":"string → mytac unit"},"response":"ok","seq_num":67}
{"record":{"source":,"state":"Custom state: ⟨y ← 20, x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":71}