michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean/whnf): make sure the test does not produce 'sorry'

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-03 21:12:33 -08:00
parent 7d19b5b743
commit b6a1c118f4
2 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/whnf.lean
View file

@ -1,4 +1,4 @@
import data.nat import data.nat.basic
open nat open nat
eval [whnf] (fun x, x + 1) 2 eval [whnf] (fun x, x + 1) 2

1
tests/lean/whnf.lean.expected.out
View file

@ -1,4 +1,3 @@
whnf.lean:2:0: warning: imported file uses 'sorry'
succ (nat.rec 2 (λ (b₁ r : ℕ), succ r) 0) succ (nat.rec 2 (λ (b₁ r : ℕ), succ r) 0)
3 3
succ (nat.rec a (λ (b₁ r : ℕ), succ r) 0) succ (nat.rec a (λ (b₁ r : ℕ), succ r) 0)