From 5180276b2a1bda0ee8025ddac65f2e92d58d6aaa Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 1 Sep 2026 13:45:17 +0000 Subject: [PATCH] fix: expose Vector DecidableEq for kernel reduction Opt the derived Vector DecidableEq helper into exposure so decide and rfl reduce across module boundaries while other derived instances remain opaque by default. --- src/Init/Data/Vector/Basic.lean | 2 +- tests/elab/vector_decidable_eq_module.lean | 9 +++++++++ 2 files changed, 10 insertions(+), 1 deletion(-) create mode 100644 tests/elab/vector_decidable_eq_module.lean diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean index 1acc8cefb72c..524b9f50721a 100644 --- a/src/Init/Data/Vector/Basic.lean +++ b/src/Init/Data/Vector/Basic.lean @@ -36,7 +36,7 @@ structure Vector (α : Type u) (n : Nat) where toArray : Array α /-- Array size. -/ size_toArray : toArray.size = n -deriving DecidableEq +deriving @[expose] DecidableEq attribute [simp, grind =] Vector.size_toArray diff --git a/tests/elab/vector_decidable_eq_module.lean b/tests/elab/vector_decidable_eq_module.lean new file mode 100644 index 000000000000..d5f052f4df7e --- /dev/null +++ b/tests/elab/vector_decidable_eq_module.lean @@ -0,0 +1,9 @@ +module + +/-! +Tests kernel reduction of derived `Vector` equality across a module boundary. +-/ + +example : (#v[] : Vector Nat 0) = #v[] := by decide +example : decide ((#v[] : Vector Nat 0) = #v[]) = true := by rfl +example : (#v[] : Vector Nat 0) = #v[] := by decide +kernel