From 92bb0468547ad460215e76adbec1b72bcbe355b6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 10 Jul 2014 15:56:15 +0100 Subject: [PATCH] test(tests/lean/run): add nested let-expr test Signed-off-by: Leonardo de Moura --- tests/lean/run/let1.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 tests/lean/run/let1.lean diff --git a/tests/lean/run/let1.lean b/tests/lean/run/let1.lean new file mode 100644 index 0000000000..38cb8b8dff --- /dev/null +++ b/tests/lean/run/let1.lean @@ -0,0 +1,10 @@ +import standard + +check + let f x y := x ∧ y, + g x := f x x, + a := g true + in λ (x : a), + let h x y := f x (g y), + b := h + in b