From 0fcb6495d6316981688b77c8dd5a213fd1e09b05 Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Fri, 20 Jun 2025 14:44:09 -0700
Subject: [PATCH] chore: add a test for #6957, fixed by the new compiler
 (#8904)

---
 tests/lean/run/6957.lean | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 tests/lean/run/6957.lean

diff --git a/tests/lean/run/6957.lean b/tests/lean/run/6957.lean
new file mode 100644
index 0000000000..50190209ce
--- /dev/null
+++ b/tests/lean/run/6957.lean
@@ -0,0 +1,6 @@
+set_option linter.unusedVariables false
+
+example (x : Nat) : Option Nat := do
+  let ⟨a, ha⟩ ← Option.attach (guard (x < 10))
+  return 0
+