From 1c77122fd0f4136f92d15fca1326f7b0e45e967d Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 18 May 2015 18:40:43 -0400 Subject: [PATCH] fix(tests): update tests because [unfold-c] attribute has been added to some definitions --- tests/lean/487.hlean.expected.out | 2 +- tests/lean/run/rewrite8.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/lean/487.hlean.expected.out b/tests/lean/487.hlean.expected.out index bc54dc13f..e084b8555 100644 --- a/tests/lean/487.hlean.expected.out +++ b/tests/lean/487.hlean.expected.out @@ -5,7 +5,7 @@ f : A → B, g : B → A, ε : Π (b : B), f (g b) = b, b b' : B -⊢ (ε b)⁻¹ ⬝ refl (f (g b)) ⬝ ε b = refl b +⊢ (ε b)⁻¹ ⬝ ε b = refl b 487.hlean:19:0: error: failed to add declaration 'foo' to environment, value has metavariables remark: set 'formatter.hide_full_terms' to false to see the complete term λ (A : Type) (B : Type) (f : …) (g : …) (ε : …) (b b' : B), diff --git a/tests/lean/run/rewrite8.lean b/tests/lean/run/rewrite8.lean index 3818cb050..c398f6d3c 100644 --- a/tests/lean/run/rewrite8.lean +++ b/tests/lean/run/rewrite8.lean @@ -3,4 +3,4 @@ open nat constant f : nat → nat theorem tst1 (x y : nat) (H1 : (λ z, z + 0) x = y) : f x = f y := -by rewrite [▸* at H1, ^add at H1, ^nat.rec_on at H1, ^of_num at H1, H1] +by rewrite [▸* at H1, ^add at H1, H1]