From cfbefd993bebd0955503a6e1485774ed468db2ef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 12 Aug 2022 10:20:17 -0700 Subject: [PATCH] fix: `lambdaBoundedTelescope` at `Compiler/Check.lean` --- src/Lean/Compiler/Check.lean | 2 +- tests/lean/run/lcnf1.lean | 11 +++++++++++ 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/src/Lean/Compiler/Check.lean b/src/Lean/Compiler/Check.lean index da09933b9b..e095bb283f 100644 --- a/src/Lean/Compiler/Check.lean +++ b/src/Lean/Compiler/Check.lean @@ -21,7 +21,7 @@ def lambdaBoundedTelescope (e : Expr) (n : Nat) (k : Array Expr → Expr → Inf where go (e : Expr) (i : Nat) (xs : Array Expr) : InferTypeM α := match i with - | 0 => k xs e + | 0 => k xs (e.instantiateRev xs) | i+1 => match e with | .lam n d b bi => withLocalDecl n (d.instantiateRev xs) bi fun x => go b i (xs.push x) diff --git a/tests/lean/run/lcnf1.lean b/tests/lean/run/lcnf1.lean index 60e4da001e..e8f5a10985 100644 --- a/tests/lean/run/lcnf1.lean +++ b/tests/lean/run/lcnf1.lean @@ -50,3 +50,14 @@ def Vec.head : Vec α (n+1) → α set_option profiler true set_option trace.Compiler.step true #eval Compiler.compile #[``Lean.Meta.isExprDefEqAuxImpl] + +def foo (a b : Nat) := + let d := match a with + | .zero => b + | .succ c => c + let e := match b with + | .zero => a + | .succ f => f + Nat.add d e + +#eval Compiler.compile #[``foo]