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

fix: typo

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-19 12:03:13 -08:00
parent eb24ec56dc
commit ea2cebaf74
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Util/WHNF.lean
View file

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