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

chore: add test for #11655 (#11718)

Browse source 
This PR adds a test for issue #11655, which it seems was fixed by #11695

Fixes #11655
This commit is contained in:
Joachim Breitner 2025-12-17 16:54:16 +01:00 • committed by GitHub
parent 08c87b2ad3
commit 1918d4f0dc
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
tests/lean/run/issue11655.lean Normal file
View file

@ -0,0 +1,7 @@
inductive T : Bool → Type
| mkTrue : T true
| mkFalse : T false
def test2 : (b : Bool) → T b → (bif b then Nat else List Nat) → Nat
| .(true), T.mkTrue, Nat.zero => 1
| _, _, _ => 0