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

fix: bug at trivialStructToMono

Browse source
This commit is contained in:
Leonardo de Moura 2022-10-06 06:10:17 -07:00
parent 08bfb7060d
commit d409ad75b5
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Compiler/LCNF/ToMono.lean
View file

@ -102,11 +102,11 @@ partial def trivialStructToMono (info : TrivialStructureInfo) (c : Cases) : Comp
assert! ctorName == info.ctorName
assert! info.fieldIdx < ps.size
let p := ps[info.fieldIdx]!
let k ← k.toMono
eraseParams ps
/- We reuse `p`s `fvarId` to avoid substitution -/
let decl := { fvarId := p.fvarId, binderName := p.binderName, type := (← p.type.toMono), value := .fvar c.discr }
let decl := { fvarId := p.fvarId, binderName := p.binderName, type := (← toMonoType p.type), value := .fvar c.discr }
modifyLCtx fun lctx => lctx.addLetDecl decl
let k ← k.toMono
return .let decl k
partial def Code.toMono (code : Code) : CompilerM Code := do