max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(tests/lean/run): fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2017-02-17 19:55:49 -08:00
parent a9122a2c0a
commit 98b2eb893d
2 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/run/dsimp_test.lean
View file

@ -10,6 +10,8 @@ do e ← to_expr p, guard (t = e)
meta def check_target (p : pexpr) : tactic unit :=
do t ← target, check_expr p t
local attribute [-simp] map head
example (a b c : nat) : head (map f [1, 2, 3]) = 20 :=
begin
dsimp [map],

6
tests/lean/run/whenIO.lean
View file

@ -1,7 +1,7 @@
import system.io
definition when (b : bool) (a : io unit) : io unit :=
definition iowhen (b : bool) (a : io unit) : io unit :=
if b = tt then a else return ()
vm_eval when tt (put_str "hello\n")
vm_eval when ff (put_str "error\n")
vm_eval iowhen tt (put_str "hello\n")
vm_eval iowhen ff (put_str "error\n")