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 +