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

perf: missing cache at whnfImp

Browse source
This commit is contained in:
Leonardo de Moura 2023-10-08 17:22:14 -07:00
parent ce4ae37c19
commit 9f50f44eed
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -871,8 +871,8 @@ partial def whnfImp (e : Expr) : MetaM Expr :=
| some v => cache useCache e v
| none =>
match (← unfoldDefinition? e') with
| some e => whnfImp e
| none => cache useCache e e'
| some e'' => cache useCache e (← whnfImp e'')
| none => cache useCache e e'
/-- If `e` is a projection function that satisfies `p`, then reduce it -/
def reduceProjOf? (e : Expr) (p : Name → Bool) : MetaM (Option Expr) := do