Zulip Chat Archive
Stream: general
Topic: slick minimum
Keeley Hoek (Sep 13 2018 at 14:20):
Is there a slick mathlib way to get the minimum/maximum element of a list given a has_lt on that list?
Patrick Massot (Sep 13 2018 at 14:21):
There is a sort file somewhere
Patrick Massot (Sep 13 2018 at 14:22):
https://github.com/leanprover/mathlib/blob/master/data/list/sort.lean
Last updated: May 02 2025 at 03:31 UTC