Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 29 insertions, 0 deletions

diff --git a/test-suite/complexity/lettuple.v b/test-suite/complexity/lettuple.v
new file mode 100644
index 00000000..0690459f
--- /dev/null
+++ b/test-suite/complexity/lettuple.v
@@ -0,0 +1,29 @@
+(* This example checks if printing nested let-in's stays in linear time *)
+(* Expected time < 1.00s *)
+
+Definition f (x : nat * nat) :=
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  0.
+
+Timeout 5 Time Print f.