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

fix: recursively process jmp args in LCNF.toMono (#8521)

Browse source 
This PR makes LCNF.toMono recursively process jmp args.
This commit is contained in:
Cameron Zwarich 2025-05-28 13:56:03 -07:00 • committed by GitHub
parent c3a010a938
commit 5814c1e757
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -221,7 +221,8 @@ partial def Code.toMono (code : Code) : ToMonoM Code := do
| .let decl k => return code.updateLet! (← decl.toMono) (← k.toMono)
| .fun decl k | .jp decl k => return code.updateFun! (← decl.toMono) (← k.toMono)
| .unreach type => return .unreach (← toMonoType type)
| .return .. | .jmp .. => return code
| .jmp fvarId args => return code.updateJmp! fvarId (← args.mapM argToMono)
| .return .. => return code
| .cases c =>
if h : c.typeName == ``Decidable then
decToMono c h