From acee5719af2328646987ea6e70e2b0c4dd325096 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Mar 2020 14:29:09 -0700
Subject: [PATCH] test: proofs by reflection

---
 tests/lean/run/reduce1.lean | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/tests/lean/run/reduce1.lean b/tests/lean/run/reduce1.lean
index 1d99a1ede7..b545da51b8 100644
--- a/tests/lean/run/reduce1.lean
+++ b/tests/lean/run/reduce1.lean
@@ -6,18 +6,18 @@ def fact : Nat → Nat
 
 new_frontend
 
-def v1 : Nat := fact 10
+abbrev v1 : Nat := fact 10
 
 theorem tst1 : Lean.reduceNat v1 = 3628800 :=
 rfl
 
-def v2 : Bool := 10000000000000000 < 200000000000000000000
-
-theorem tst2 : Lean.reduceBool v2 = true :=
-rfl
-
-theorem tst3 : v1 = 3628800 :=
+theorem tst2 : fact 10 = 3628800 :=
 Lean.ofReduceNat v1 3628800 rfl
 
-theorem tst4 : v2 = true :=
+abbrev v2 : Bool := decide (10000000000000000 < 200000000000000000000)
+
+theorem tst3 : Lean.reduceBool v2 = true :=
+rfl
+
+theorem tst4 : decide (10000000000000000 < 200000000000000000000) = true :=
 Lean.ofReduceBool v2 true rfl