diff --git a/src/Lean/Compiler/LCNF.lean b/src/Lean/Compiler/LCNF.lean index 30c9fc5284..f555477ece 100644 --- a/src/Lean/Compiler/LCNF.lean +++ b/src/Lean/Compiler/LCNF.lean @@ -440,7 +440,7 @@ where visitLet body (xs.push value) else let type' ← liftMetaM <| toLCNFType type - let value' ← visitChild value + let value' ← visit value let x ← mkLetDecl binderName type value type' value' visitLet body (xs.push x) | _ => diff --git a/tests/lean/run/lcnf2.lean b/tests/lean/run/lcnf2.lean index b44b9e7eca..e367f40b94 100644 --- a/tests/lean/run/lcnf2.lean +++ b/tests/lean/run/lcnf2.lean @@ -33,3 +33,10 @@ noncomputable abbrev TupleN : (n : Fin 1) → TupleNTyp n.val set_option pp.proofs true #eval Compiler.compile #[``TupleN] + + +def userControlled (a b : Nat) := + let f := fun _ => a + f () + b + +#eval Compiler.compile #[``userControlled]