Array.qsort and `≥`

Stream: lean4

[Damiano Testa]

Dear All,

I find the first example below a little surprising.

import Init.Data.Array.QSort

#eval Array.qsort #[1, 1, 2, 1] (· ≥ ·) == #[1, 1, 2, 1]
-- true

#eval Array.qsort #[1, 1, 2, 1] (· ≤ ·) == #[1, 1, 2, 1]
-- false

I know that ≥ is unwanted in Mathlib, but I thought that it was mostly motivated in order to avoid code-duplication. :smile:

[Mario Carneiro]

note that the function seems to be expecting an irreflexive relation (lt)

[Damiano Testa]

Ok, with > it works as expected, thanks!