From 6290919170e898ec92e6d48954593703bb1fc765 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Fri, 13 Nov 2015 11:31:18 -0800 Subject: [PATCH] test(tests/lean/simplifier_norm_num): add moderate sized test --- tests/lean/simplifier13.lean | 5 ++--- tests/lean/simplifier_norm_num.lean | 2 ++ tests/lean/simplifier_norm_num.lean.expected.out | 1 + 3 files changed, 5 insertions(+), 3 deletions(-) diff --git a/tests/lean/simplifier13.lean b/tests/lean/simplifier13.lean index fd79be4db..9876acca3 100644 --- a/tests/lean/simplifier13.lean +++ b/tests/lean/simplifier13.lean @@ -1,10 +1,9 @@ universe l -constants (T : Type.{l}) (f : T → T → T) (g : T → T) +constants (T : Type.{l}) (f : T → T → T) (g : T → T) constants (P : T → Prop) (Q : Prop) (Hfg : ∀ (x : T), f x x = g x) -constants (c : Π (x y z : T), P x → P y → P z → Q) +constants (c : Π (x y z : T), P x → P y → P z → Q) constants (x y z : T) (px : P (f x x)) (py : P (f y y)) (pz : P (g z)) attribute Hfg [simp] #simplify eq 0 c (f x x) (f y y) (g z) px py pz - diff --git a/tests/lean/simplifier_norm_num.lean b/tests/lean/simplifier_norm_num.lean index 027608b6a..ab46c46db 100644 --- a/tests/lean/simplifier_norm_num.lean +++ b/tests/lean/simplifier_norm_num.lean @@ -52,5 +52,7 @@ attribute A_comm_ring [instance] #simplify eq 0 (15 : A) * 6 #simplify eq 0 (123456 : A) * 123456 +#simplify eq 0 (0 + 45343453:A) * (53653343 + 1) * (53453 + 2) + (0 + 1 + 2 + 2200000000034733) + -- The following test is too slow -- #simplify eq 0 (23000000000343434534345316:A) * (53653343563534534 + 5367536453653573573453) * 53453756475777536 + 2200000000034733531531531534536 diff --git a/tests/lean/simplifier_norm_num.lean.expected.out b/tests/lean/simplifier_norm_num.lean.expected.out index 7aefaf890..3b82bbf47 100644 --- a/tests/lean/simplifier_norm_num.lean.expected.out +++ b/tests/lean/simplifier_norm_num.lean.expected.out @@ -39,3 +39,4 @@ 22 90 15241383936 +130049014430002489296