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

fix: nasty bug due to #1804

Browse source
This commit is contained in:
Leonardo de Moura 2022-11-06 18:14:23 -08:00
parent c5584581ce
commit cf13b29760
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/Lean/Compiler/LCNF/ReduceArity.lean
View file

@ -124,7 +124,7 @@ abbrev ReduceM := ReaderT Context CompilerM
partial def reduce (code : Code) : ReduceM Code := do
match code with
| .let decl k =>
let .const declName _ args := decl.value | return code.updateLet! decl (← reduce k)
let .const declName _ args := decl.value | do return code.updateLet! decl (← reduce k)
unless declName == (← read).declName do return code.updateLet! decl (← reduce k)
let mut argsNew := #[]
for used in (← read).paramMask, arg in args do