From 98b2eb893df826ccae4840f3fc624c583ee086a0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Feb 2017 19:55:49 -0800 Subject: [PATCH] chore(tests/lean/run): fix tests --- tests/lean/run/dsimp_test.lean | 2 ++ tests/lean/run/whenIO.lean | 6 +++--- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/tests/lean/run/dsimp_test.lean b/tests/lean/run/dsimp_test.lean index 6e6e51c56f..749d12ce3b 100644 --- a/tests/lean/run/dsimp_test.lean +++ b/tests/lean/run/dsimp_test.lean @@ -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], diff --git a/tests/lean/run/whenIO.lean b/tests/lean/run/whenIO.lean index 9e36074a4e..83f3e84494 100644 --- a/tests/lean/run/whenIO.lean +++ b/tests/lean/run/whenIO.lean @@ -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")