why is < Prop-valued instead of a Bool?

Stream: new members

[Alok Singh]

This has caused random issues, and is unlike most programming languages (not that most programming languages have Prop at all). I would have thought it'd be implemented through Ord, but in fact Ord seems to use the less than under the hood:

/--
Yields an `Ordering` s.t. `x < y` corresponds to `Ordering.lt` / `Ordering.gt` and
`x = y` corresponds to `Ordering.eq`.
-/
@[inline] def compareOfLessAndEq {α} (x y : α) [LT α] [Decidable (x < y)] [DecidableEq α] : Ordering :=
  if x < y then Ordering.lt
  else if x = y then Ordering.eq
  else Ordering.gt

[Daniel Weber]

Do you have an example of an issue this has caused? Ord can also be implemented independently, but in many cases when you're proving proofs you don't want to use Ord

[Alok Singh]

I'll look for one, but it's more that when I've used it, it's been for
ordinary programming over proving. So the decidableeq condition becomes
annoying, especially with floats. It's been a few months, but my library
github.com/alok/lean-inf had some issues with that.

[Daniel Weber]

I think you're supposed to use docs#BEq instead of DecidableEq for floats. I don't think there's a similar variant for LT, but note that you can define it however you feel like