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

chore: remove unnecessary auxiliary declaration

Browse source
This commit is contained in:
Leonardo de Moura 2022-11-06 17:15:47 -08:00
parent 46d83f2d80
commit 0cfdf285e3
1 changed files with 20 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
src/Lean/Compiler/LCNF/Simp/Main.lean
View file

@ -303,26 +303,24 @@ partial def simp (code : Code) : SimpM Code := withIncRecDepth do
if let some k ← simpCasesOnCtor? c then
return k
else
let simpCasesDefault := do
let discr ← normFVar c.discr
let resultType ← normExpr c.resultType
markUsedFVar discr
let alts ← c.alts.mapMonoM fun alt => do
match alt with
| .alt ctorName ps k =>
if !(k matches .unreach ..) && (← ps.anyM fun p => isInductiveWithNoCtors p.type) then
let type ← k.inferType
eraseCode k
markSimplified
return alt.updateCode (.unreach type)
else
withDiscrCtor discr ctorName ps do
return alt.updateCode (← simp k)
| .default k => return alt.updateCode (← simp k)
let alts ← addDefaultAlt alts
if alts.size == 1 && alts[0]! matches .default .. then
return alts[0]!.getCode
else
return code.updateCases! resultType discr alts
simpCasesDefault
let discr ← normFVar c.discr
let resultType ← normExpr c.resultType
markUsedFVar discr
let alts ← c.alts.mapMonoM fun alt => do
match alt with
| .alt ctorName ps k =>
if !(k matches .unreach ..) && (← ps.anyM fun p => isInductiveWithNoCtors p.type) then
let type ← k.inferType
eraseCode k
markSimplified
return alt.updateCode (.unreach type)
else
withDiscrCtor discr ctorName ps do
return alt.updateCode (← simp k)
| .default k => return alt.updateCode (← simp k)
let alts ← addDefaultAlt alts
if alts.size == 1 && alts[0]! matches .default .. then
return alts[0]!.getCode
else
return code.updateCases! resultType discr alts
end