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

chore: use toExpr

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-18 10:26:32 -07:00
parent b4942fcd30
commit 84f856bed9
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/Lean/Meta/WHNF.lean
View file

@ -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