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