diff --git a/tests/lean/vm_let_expr.lean b/tests/lean/vm_let_expr.lean
new file mode 100644
index 0000000000..94001f0d86
--- /dev/null
+++ b/tests/lean/vm_let_expr.lean
@@ -0,0 +1,11 @@
+meta def mk_value (n : nat) : nat :=
+trace "mk_value" (λ _, 2 * n)
+
+meta def mk_fn (sz : nat) : nat → nat :=
+let n := mk_value sz in
+λ x, x + n
+
+vm_eval let f := mk_fn 10 in f 1 + f 2 + f 3 + f 4
+
+
+vm_eval ((let x := mk_value 10 in mk_fn x) 10)
diff --git a/tests/lean/vm_let_expr.lean.expected.out b/tests/lean/vm_let_expr.lean.expected.out
new file mode 100644
index 0000000000..b03acbdfd8
--- /dev/null
+++ b/tests/lean/vm_let_expr.lean.expected.out
@@ -0,0 +1,5 @@
+mk_value
+90
+mk_value
+mk_value
+50