From 1918d4f0dcbedc6978def18560cef39167d033d1 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 17 Dec 2025 16:54:16 +0100
Subject: [PATCH] chore: add test for #11655 (#11718)

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

Fixes #11655
---
 tests/lean/run/issue11655.lean | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 tests/lean/run/issue11655.lean

diff --git a/tests/lean/run/issue11655.lean b/tests/lean/run/issue11655.lean
new file mode 100644
index 0000000000..a4bf37f0ae
--- /dev/null
+++ b/tests/lean/run/issue11655.lean
@@ -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