From 8d8c73416adc63759d58e07f8a71dce75248927f Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Fri, 20 Jun 2025 10:37:19 -0700 Subject: [PATCH] chore: add a test for #2602, which was fixed by the new compiler (#8902) --- tests/lean/run/2602.lean | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 tests/lean/run/2602.lean diff --git a/tests/lean/run/2602.lean b/tests/lean/run/2602.lean new file mode 100644 index 0000000000..c1d11599ab --- /dev/null +++ b/tests/lean/run/2602.lean @@ -0,0 +1,13 @@ +inductive Units : Bool → Type where +| seconds : Units false +| hours : Units true + +open Units + +structure Quantity (d : Bool) : Type where + quantity : Unit + units : Units d + +instance (d : Bool) : ToString (Quantity d) where + toString q := match q.units with | seconds => "seconds" | hours => "hours" +