From cdfa9e655c35621e8d82a14bcdadd6e13e6dcd4d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Jan 2017 08:50:45 -0800 Subject: [PATCH] test(tests/lean/vm_let_expr): add regression test for bugs fixed in the previous two commits --- tests/lean/vm_let_expr.lean | 11 +++++++++++ tests/lean/vm_let_expr.lean.expected.out | 5 +++++ 2 files changed, 16 insertions(+) create mode 100644 tests/lean/vm_let_expr.lean create mode 100644 tests/lean/vm_let_expr.lean.expected.out 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