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

fix: incorrect binder name being used

Browse source 
cc @hargoniX
This commit is contained in:
Leonardo de Moura 2022-09-04 16:56:42 -07:00
parent abd37d8fd1
commit d0600b3750
2 changed files with 11 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Compiler/LCNF/InferType.lean
View file

@ -202,9 +202,8 @@ def mkAuxJpDecl (params : Array Param) (code : Code) (prefixName := `_jp) : Comp
mkAuxFunDecl params code prefixName
def mkAuxJpDecl' (fvarId : FVarId) (code : Code) (prefixName := `_jp) : CompilerM FunDecl := do
let y ← mkFreshBinderName `_y
let yType ← inferType (.fvar fvarId)
let params := #[{ fvarId, binderName := y, type := yType }]
let localDecl ← getLocalDecl fvarId
let params := #[{ fvarId, binderName := localDecl.userName, type := localDecl.type }]
mkAuxFunDecl params code prefixName
def instantiateForall (type : Expr) (params : Array Param) : CoreM Expr :=

9
tests/lean/run/lcnfBinderNameBug.lean Normal file
View file

@ -0,0 +1,9 @@
import Lean
def test (a : Nat) :=
let foo := match a with
| .zero => a
| .succ b => b
Nat.add foo .zero
#eval Lean.Compiler.compile #[``test]