From 84f856bed9b1bd55686ff5c9adccf3c020b92928 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 18 Mar 2020 10:26:32 -0700
Subject: [PATCH] chore: use `toExpr`

---
 src/Init/Lean/Meta/WHNF.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Init/Lean/Meta/WHNF.lean b/src/Init/Lean/Meta/WHNF.lean
index 5ff5f8f679..f78ac35fae 100644
--- a/src/Init/Lean/Meta/WHNF.lean
+++ b/src/Init/Lean/Meta/WHNF.lean
@@ -37,10 +37,10 @@ match e with
 | Expr.app (Expr.const fName _ _) (Expr.const argName _ _) _ =>
   if fName == `Lean.reduceBool then do
     b ← reduceBoolNative argName;
-    pure $ if b then some $ mkConst `Bool.true else some $ mkConst `Bool.false
+    pure $ toExpr b
   else if fName == `Lean.reduceNat then do
     n ← reduceNatNative argName;
-    pure $ some $ mkNatLit n
+    pure $ toExpr n
   else
     pure none
 | _ => pure none
@@ -65,7 +65,7 @@ pure $ mkNatLit $ f a b
 def reduceBinNatPred (f : Nat → Nat → Bool) (a b : Expr) : MetaM (Option Expr) := do
 withNatValue a $ fun a =>
 withNatValue b $ fun b =>
-pure $ some $ if f a b then mkConst `Bool.true else mkConst `Bool.false
+pure $ toExpr $ f a b
 
 def reduceNat? (e : Expr) : MetaM (Option Expr) :=
 if e.hasFVar || e.hasMVar then