Zulip Chat Archive

Stream: mathlib4

Topic: Insert for `List _`

Yury G. Kudryashov (Sep 30 2025 at 00:15):

Should we drop the Singleton and Insert instances for List? They are almost unused @loogle ({_} : List _)

loogle (Sep 30 2025 at 00:15):

:search: List.singleton_eq, List.doubleton_eq

Yury G. Kudryashov (Sep 30 2025 at 00:15):

@loogle (Insert.insert _ _ : List _)

loogle (Sep 30 2025 at 00:15):

:search: List.insert_pos, List.insert_neg, and 3 more

Yury G. Kudryashov (Sep 30 2025 at 00:16):

Lean core uses List.insert instead.

Last updated: Dec 20 2025 at 21:32 UTC