From 1c00f290430e86e4b63083d5c64fe51657bd2568 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 16 Sep 2021 10:14:42 -0700
Subject: [PATCH] test: add `let_fun` pretty printing test

---
 tests/lean/letFun.lean              | 10 ++++++++++
 tests/lean/letFun.lean.expected.out | 10 ++++++++++
 2 files changed, 20 insertions(+)
 create mode 100644 tests/lean/letFun.lean
 create mode 100644 tests/lean/letFun.lean.expected.out

diff --git a/tests/lean/letFun.lean b/tests/lean/letFun.lean
new file mode 100644
index 0000000000..0da44ce333
--- /dev/null
+++ b/tests/lean/letFun.lean
@@ -0,0 +1,10 @@
+#check
+  let_fun f x := x * 2
+  let_fun x := 1
+  let_fun y := x + 1
+  f (y + x)
+
+example (a b : Nat) (h1 : a = 0) (h2 : b = 0) : (let_fun x := a + 1; x + x) > b := by
+  simp (config := { beta := false }) [h1]
+  traceState
+  simp [h2]
diff --git a/tests/lean/letFun.lean.expected.out b/tests/lean/letFun.lean.expected.out
new file mode 100644
index 0000000000..9d4337b024
--- /dev/null
+++ b/tests/lean/letFun.lean.expected.out
@@ -0,0 +1,10 @@
+let_fun f := fun x => x * 2;
+let_fun x := 1;
+let_fun y := x + 1;
+f (y + x) : Nat
+a b : Nat
+h1 : a = 0
+h2 : b = 0
+⊢ (let_fun x := 1;
+    x + x) >
+    b