From a9f7d87aae2c6576314b9932a7345e1474d6d6a5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Jul 2014 05:58:36 -0700 Subject: [PATCH] test(tests/lean/run/decidable): show implicit argument that is computed automatically Signed-off-by: Leonardo de Moura --- tests/lean/run/decidable.lean | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/tests/lean/run/decidable.lean b/tests/lean/run/decidable.lean index a72f5686b..f2a450a7e 100644 --- a/tests/lean/run/decidable.lean +++ b/tests/lean/run/decidable.lean @@ -1,11 +1,7 @@ -import standard unit decidable +import standard unit decidable if using bit unit decidable variables a b c : bit variables u v : unit - -theorem tst : decidable ((a = b) ∧ (b = c) → ¬ (u = v) ∨ (a = c) → (a = c) ↔ a = '1 ↔ true) - -(* -print(get_env():find("tst"):value()) -*) +set_option pp.implicit true +check if ((a = b) ∧ (b = c) → ¬ (u = v) ∨ (a = c) → (a = c) ↔ a = '1 ↔ true) then a else b