From 620ef3bb86dce4254469704d7b8f9fccbad07c23 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 16 Feb 2026 14:33:10 +0100 Subject: [PATCH] fix: bring lengthTR lemma back into scope at toArray (#12502) This PR brings the `length = lengthTR` lemma back into scope after shake mistakenly removed it. --- src/Init/Data/List/ToArrayImpl.lean | 1 + tests/lean/run/to_array_csimp.lean | 5 +++++ 2 files changed, 6 insertions(+) create mode 100644 tests/lean/run/to_array_csimp.lean diff --git a/src/Init/Data/List/ToArrayImpl.lean b/src/Init/Data/List/ToArrayImpl.lean index 6847221baf..d357476552 100644 --- a/src/Init/Data/List/ToArrayImpl.lean +++ b/src/Init/Data/List/ToArrayImpl.lean @@ -7,6 +7,7 @@ module prelude public import Init.Prelude +import Init.Data.List.Basic public section diff --git a/tests/lean/run/to_array_csimp.lean b/tests/lean/run/to_array_csimp.lean new file mode 100644 index 0000000000..2c7ad7914c --- /dev/null +++ b/tests/lean/run/to_array_csimp.lean @@ -0,0 +1,5 @@ +/-! regression test against missing csimp lemmas in Init -/ + +/-- info: 300000 -/ +#guard_msgs in +#eval (List.range (3 * 10 ^ 5)).toArray.size