From 1ac240e2db9bdcda1b9ac5378cdeba5da70915c0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Mar 2017 19:45:00 -0800 Subject: [PATCH] chore(tests/lean): fix tests --- .../lean/interactive/complete_field.lean.expected.out | 6 +++--- tests/lean/run/1335.lean | 10 +++++----- tests/lean/run/soundness.lean | 2 +- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/tests/lean/interactive/complete_field.lean.expected.out b/tests/lean/interactive/complete_field.lean.expected.out index ec19306aa5..6df64d0b20 100644 --- a/tests/lean/interactive/complete_field.lean.expected.out +++ b/tests/lean/interactive/complete_field.lean.expected.out @@ -3,7 +3,7 @@ {"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":12,"severity":"error","text":"invalid '^.' notation, 'r' is not a valid \"field\" because environment does not contain 'and.r'\n h y\nwhich has type\n p y ∧ q y"},"response":"additional_message"} {"msg":{"caption":"","file_name":"f","pos_col":39,"pos_line":17,"severity":"error","text":"invalid '^.' notation, identifier or numeral expected"},"response":"additional_message"} {"message":"file invalidated","response":"ok","seq_num":0} -{"completions":[{"source":,"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":408},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"l","response":"ok","seq_num":5} -{"completions":[{"source":,"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":408},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"le","response":"ok","seq_num":9} +{"completions":[{"source":,"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":411},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"l","response":"ok","seq_num":5} +{"completions":[{"source":,"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":411},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"le","response":"ok","seq_num":9} {"completions":[{"source":,"text":"rec","type":"(?a → ?b → ?C) → ?a ∧ ?b → ?C"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"rec_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":4,"file":"/library/init/core.lean","line":144},"text":"right","type":"?a ∧ ?b → ?b"}],"prefix":"r","response":"ok","seq_num":13} -{"completions":[{"source":,"text":"assoc","type":"(?a ∧ ?b) ∧ ?c ↔ ?a ∧ ?b ∧ ?c"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"cases_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":14,"file":"/library/init/logic.lean","line":396},"text":"comm","type":"?a ∧ ?b ↔ ?b ∧ ?a"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"dcases_on","type":"Π (n : ?a ∧ ?b), (Π (a : ?a) (a_1 : ?b), ?C (and.intro a a_1)) → ?C n"},{"source":{"column":11,"file":"/library/init/logic.lean","line":656},"text":"decidable","type":"decidable (?p ∧ ?q)"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"drec","type":"(Π (a : ?a) (a_1 : ?b), ?C (and.intro a a_1)) → Π (n : ?a ∧ ?b), ?C n"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"drec_on","type":"Π (n : ?a ∧ ?b), (Π (a : ?a) (a_1 : ?b), ?C (and.intro a a_1)) → ?C n"},{"source":{"column":6,"file":"/library/init/logic.lean","line":207},"text":"elim","type":"?a ∧ ?b → (?a → ?b → ?c) → ?c"},{"source":{"column":4,"file":"/library/init/core.lean","line":136},"text":"elim_left","type":"?a ∧ ?b → ?a"},{"source":{"column":4,"file":"/library/init/core.lean","line":141},"text":"elim_right","type":"?a ∧ ?b → ?b"},{"source":{"column":6,"file":"/library/init/logic.lean","line":383},"text":"imp","type":"(?a → ?c) → (?b → ?d) → ?a ∧ ?b → ?c ∧ ?d"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"induction_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"intro","type":"?a → ?b → ?a ∧ ?b"},{"source":{"column":4,"file":"/library/init/core.lean","line":139},"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":408},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"rec","type":"(?a → ?b → ?C) → ?a ∧ ?b → ?C"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"rec_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":4,"file":"/library/init/core.lean","line":144},"text":"right","type":"?a ∧ ?b → ?b"},{"source":{"column":6,"file":"/library/init/logic.lean","line":210},"text":"swap","type":"?a ∧ ?b → ?b ∧ ?a"},{"source":{"column":4,"file":"/library/init/logic.lean","line":213},"text":"symm","type":"?a ∧ ?b → ?b ∧ ?a"}],"prefix":"","response":"ok","seq_num":17} +{"completions":[{"source":,"text":"assoc","type":"(?a ∧ ?b) ∧ ?c ↔ ?a ∧ ?b ∧ ?c"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"cases_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":14,"file":"/library/init/logic.lean","line":399},"text":"comm","type":"?a ∧ ?b ↔ ?b ∧ ?a"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"dcases_on","type":"Π (n : ?a ∧ ?b), (Π (a : ?a) (a_1 : ?b), ?C (and.intro a a_1)) → ?C n"},{"source":{"column":11,"file":"/library/init/logic.lean","line":659},"text":"decidable","type":"decidable (?p ∧ ?q)"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"drec","type":"(Π (a : ?a) (a_1 : ?b), ?C (and.intro a a_1)) → Π (n : ?a ∧ ?b), ?C n"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"drec_on","type":"Π (n : ?a ∧ ?b), (Π (a : ?a) (a_1 : ?b), ?C (and.intro a a_1)) → ?C n"},{"source":{"column":6,"file":"/library/init/logic.lean","line":207},"text":"elim","type":"?a ∧ ?b → (?a → ?b → ?c) → ?c"},{"source":{"column":4,"file":"/library/init/core.lean","line":136},"text":"elim_left","type":"?a ∧ ?b → ?a"},{"source":{"column":4,"file":"/library/init/core.lean","line":141},"text":"elim_right","type":"?a ∧ ?b → ?b"},{"source":{"column":6,"file":"/library/init/logic.lean","line":386},"text":"imp","type":"(?a → ?c) → (?b → ?d) → ?a ∧ ?b → ?c ∧ ?d"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"induction_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"intro","type":"?a → ?b → ?a ∧ ?b"},{"source":{"column":4,"file":"/library/init/core.lean","line":139},"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":411},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"rec","type":"(?a → ?b → ?C) → ?a ∧ ?b → ?C"},{"source":{"column":10,"file":"/library/init/core.lean","line":133},"text":"rec_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":4,"file":"/library/init/core.lean","line":144},"text":"right","type":"?a ∧ ?b → ?b"},{"source":{"column":6,"file":"/library/init/logic.lean","line":210},"text":"swap","type":"?a ∧ ?b → ?b ∧ ?a"},{"source":{"column":4,"file":"/library/init/logic.lean","line":213},"text":"symm","type":"?a ∧ ?b → ?b ∧ ?a"}],"prefix":"","response":"ok","seq_num":17} diff --git a/tests/lean/run/1335.lean b/tests/lean/run/1335.lean index 4da99f493e..2b49af8370 100644 --- a/tests/lean/run/1335.lean +++ b/tests/lean/run/1335.lean @@ -7,12 +7,12 @@ private lemma sub_nat_nat_elim (m n : ℕ) (P : ℕ → ℕ → ℤ → Prop) P m n (sub_nat_nat m n) := sorry -inductive rel_int_nat_nat : ℤ → ℕ × ℕ → Prop -| pos : ∀m p, rel_int_nat_nat (of_nat p) (m + p, m) -| neg : ∀m n, rel_int_nat_nat (neg_succ_of_nat n) (m, m + n) +inductive rel_int_nat_nat__ : ℤ → ℕ × ℕ → Prop +| pos : ∀m p, rel_int_nat_nat__ (of_nat p) (m + p, m) +| neg : ∀m n, rel_int_nat_nat__ (neg_succ_of_nat n) (m, m + n) -lemma rel_sub_nat_nat {a b : ℕ} : rel_int_nat_nat (sub_nat_nat a b) (a, b) := +lemma rel_sub_nat_nat__ {a b : ℕ} : rel_int_nat_nat__ (sub_nat_nat a b) (a, b) := /- The next statement kills lean -/ -sub_nat_nat_elim a b (λ(a b : ℕ) (i : ℤ), rel_int_nat_nat i (a, b)) sorry sorry +sub_nat_nat_elim a b (λ(a b : ℕ) (i : ℤ), rel_int_nat_nat__ i (a, b)) sorry sorry end int diff --git a/tests/lean/run/soundness.lean b/tests/lean/run/soundness.lean index 52adc95e22..3b82199b94 100644 --- a/tests/lean/run/soundness.lean +++ b/tests/lean/run/soundness.lean @@ -27,7 +27,7 @@ namespace PropF notation `#`:max P:max := Var P local notation A ∨ B := Disj A B local notation A ∧ B := Conj A B - infixr `⇒`:27 := Impl + local infixr `⇒`:27 := Impl notation `⊥` := Bot def Neg A := A ⇒ ⊥