max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add a test for #6957, fixed by the new compiler (#8904)

Browse source
This commit is contained in:
Cameron Zwarich 2025-06-20 14:44:09 -07:00 • committed by GitHub
parent e7c8baaef5
commit 0fcb6495d6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/run/6957.lean Normal file
View file

@ -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