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

perf: (try to) fix regression introduced by #3139

Browse source
This commit is contained in:
Leonardo de Moura 2024-01-07 10:05:35 -08:00 • committed by Sebastian Ullrich
parent b8b49c50b9
commit 29c245ceba
1 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Lean/Meta/WHNF.lean
View file

@ -827,12 +827,17 @@ def reduceNative? (e : Expr) : MetaM (Option Expr) :=
| _ =>
return none
@[inline] def withNatValue {α} (a : Expr) (k : Nat → MetaM (Option α)) : MetaM (Option α) := do
@[inline] def withNatValue (a : Expr) (k : Nat → MetaM (Option α)) : MetaM (Option α) := do
if !a.hasExprMVar && a.hasFVar then
return none
let a ← instantiateMVars a
if a.hasExprMVar || a.hasFVar then
return none
let a ← whnf a
match a with
| Expr.const `Nat.zero _ => k 0
| Expr.lit (Literal.natVal v) => k v
| _ => return none
| .const ``Nat.zero _ => k 0
| .lit (.natVal v) => k v
| _ => return none
def reduceUnaryNatOp (f : Nat → Nat) (a : Expr) : MetaM (Option Expr) :=
withNatValue a fun a =>