From ea2cebaf7415f7f6778eff778fbd489a5d0fab4b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 19 Dec 2019 12:03:13 -0800 Subject: [PATCH] fix: typo --- src/Init/Lean/Util/WHNF.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Util/WHNF.lean b/src/Init/Lean/Util/WHNF.lean index 109e95b1d8..149b175c0a 100644 --- a/src/Init/Lean/Util/WHNF.lean +++ b/src/Init/Lean/Util/WHNF.lean @@ -288,7 +288,7 @@ else f' ← whnfCore f; if f'.isLambda then let revArgs := e.getAppRevArgs; - whnfCore $ f.betaRev revArgs + whnfCore $ f'.betaRev revArgs else do let done : Unit → m Expr := fun _ => if f == f' then pure e else pure $ e.updateFn f';