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 2022-09-02 03:41:49 -07:00
parent baf4f1c152
commit dfdbec51ad
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/Simp.lean
View file

@ -332,7 +332,7 @@ where
go (i : Nat) (code : Code) : SimpM Code := do
if i > 0 then
let decl := decls[i-1]!
if decl.isPure || (← isUsed decl.fvarId) then
if !decl.isPure || (← isUsed decl.fvarId) then
match decl with
| .let decl => markUsedLetDecl decl; go (i-1) (.let decl code)
| .fun decl => markUsedFunDecl decl; go (i-1) (.fun decl code)