Zulip Chat Archive

Stream: lean4

Topic: qsort with >=


view this post on Zulip Petrica Chiriac (Jan 10 2021 at 09:29):

Second sort seems incorrect

#eval #[1, 1,3,20, -2].qsort fun a b => a > b
-- #[20, 3, 1, 1, -2]
#eval #[1, 1,3,20, -2].qsort fun a b => a >= b
-- #[3, 1, 20, 1, -2]

what is wrong here

view this post on Zulip Kenny Lau (Jan 10 2021 at 09:29):

#backticks

view this post on Zulip Mario Carneiro (Jan 10 2021 at 12:22):

Presumably the qsort implementation expects that you give it a relation that is treated as "strictly less than". If you give it a reflexive relation it will think that equal elements satisfy a < b and b < a so this will cause a bad sort


Last updated: May 07 2021 at 13:21 UTC