error msg in for loop

Stream: new members

[Alok Singh]

def Array.min [LT a](self: Array a) := Id.run do
  let mut min? := none
  for x in self do
    if let some y := min? then
      if x < y then
        min? := x

gives error msg failed to synthesize instance Decidable (x < y).

[Kevin Buzzard]

That looks expected to me -- if you want to use if then you need an algorithm.

[Damiano Testa]

... and you can fix it by adding [DecidableRel ((· < ·) : a → a → Prop)] to your assumptions.