From 8137f94b3c7350bcb8c36b4586f201a646212b25 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 1 Dec 2014 17:14:11 -0800 Subject: [PATCH] fix(tests/lean): to reflect recent changes --- tests/lean/inv_del.lean.expected.out | 6 +++--- tests/lean/no_confusion_type.lean.expected.out | 2 +- tests/lean/whnf.lean.expected.out | 6 +++--- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/tests/lean/inv_del.lean.expected.out b/tests/lean/inv_del.lean.expected.out index b2e3f5544..afd7f3c82 100644 --- a/tests/lean/inv_del.lean.expected.out +++ b/tests/lean/inv_del.lean.expected.out @@ -1,10 +1,10 @@ inv_del.lean:15:2: error: unsolved subgoals A : Type, -P : vec A (succ zero) → Type, +P : vec A 1 → Type, H : Π (a : A), P (vone a), -v : vec A (succ zero), +v : vec A 1, a : A ⊢ P (vone a) inv_del.lean:15:2: error: failed to add declaration 'vec.eone' to environment, value has metavariables - λ (A : Type) (P : vec A (succ zero) → Type) (H : Π (a : A), P (vone a)) (v : vec A (succ zero)), + λ (A : Type) (P : vec A 1 → Type) (H : Π (a : A), P (vone a)) (v : vec A 1), ?M_1 diff --git a/tests/lean/no_confusion_type.lean.expected.out b/tests/lean/no_confusion_type.lean.expected.out index 0d4c2ccb3..96cd290a8 100644 --- a/tests/lean/no_confusion_type.lean.expected.out +++ b/tests/lean/no_confusion_type.lean.expected.out @@ -1,2 +1,2 @@ vector.no_confusion_type : Type → vector ?A ?a → vector ?A ?a → Type -(succ (succ zero) = succ (succ zero) → a1 = a2 → v1 == v2 → P) → P +(2 = 2 → a1 = a2 → v1 == v2 → P) → P diff --git a/tests/lean/whnf.lean.expected.out b/tests/lean/whnf.lean.expected.out index fc0090fcc..997689320 100644 --- a/tests/lean/whnf.lean.expected.out +++ b/tests/lean/whnf.lean.expected.out @@ -1,5 +1,5 @@ whnf.lean:2:0: warning: imported file uses 'sorry' -succ (nat.rec 2 (λ (b₁ r : ℕ), succ r) zero) -succ (succ (succ zero)) -succ (nat.rec a (λ (b₁ r : ℕ), succ r) zero) +succ (nat.rec 2 (λ (b₁ r : ℕ), succ r) 0) +3 +succ (nat.rec a (λ (b₁ r : ℕ), succ r) 0) succ a