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

chore(tests/lean): fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2017-03-07 19:45:00 -08:00
parent d6eae3265c
commit 1ac240e2db
3 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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}

10
tests/lean/run/1335.lean
View file

@ -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

2
tests/lean/run/soundness.lean
View file

@ -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 ⇒ ⊥