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)