qsort with >=

Stream: lean4

[Petrica Chiriac]

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

[Kenny Lau]

#backticks

[Mario Carneiro]

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