From b6a1c118f408fc4c2c92cdbde0a4e8629d90d842 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 3 Dec 2014 21:12:33 -0800
Subject: [PATCH] fix(tests/lean/whnf): make sure the test does not produce
 'sorry'

---
 tests/lean/whnf.lean              | 2 +-
 tests/lean/whnf.lean.expected.out | 1 -
 2 files changed, 1 insertion(+), 2 deletions(-)

diff --git a/tests/lean/whnf.lean b/tests/lean/whnf.lean
index 6988f71aa..4446958da 100644
--- a/tests/lean/whnf.lean
+++ b/tests/lean/whnf.lean
@@ -1,4 +1,4 @@
-import data.nat
+import data.nat.basic
 open nat
 
 eval [whnf] (fun x, x + 1) 2
diff --git a/tests/lean/whnf.lean.expected.out b/tests/lean/whnf.lean.expected.out
index 997689320..78ee85448 100644
--- a/tests/lean/whnf.lean.expected.out
+++ b/tests/lean/whnf.lean.expected.out
@@ -1,4 +1,3 @@
-whnf.lean:2:0: warning: imported file uses 'sorry'
 succ (nat.rec 2 (λ (b₁ r : ℕ), succ r) 0)
 3
 succ (nat.rec a (λ (b₁ r : ℕ), succ r) 0)