Request: lexicographical orderings

[robin-aws]

Spun off from #49. Once that is merged we'll have the definition of [strict] total orderings, and can sensibly define this ordering for seq<T> values based on an element ordering on T values.

This is particularly valuable because Dafny defines < on string values to be "proper prefix of" to make termination proofs easier, but many many users will also want the more common definition as well.

We also need to be careful about implying that using this ordering on Dafny string values will align with the actual intentions, since char values are currently UTF-16 code units and therefore a naive lexicographic comparison will likely not be correct for most uses. This will still be true even after dafny-lang/rfcs#13 is implemented, since individual Unicode scalar values don't always correspond to human-perceived characters either. We will likely want separate stdlib utilities for Unicode-compliant collation. See https://unicode.org/reports/tr10/ for the gory details.

[kjx]

I also got caught out by this; thinking "<" on strings meant the same as it does in pretty much *every other programming language in the known universe". Would be good to have T(<) to mean Comparable long with T(==) Equality bounds on generic parameters, and potentially a notion (where clauses per attribute) that means a sequence of comparable elements is itself comparable (or whatever the haskell terminology is).

probably have to pick some other operators for "isPrefixOf" though... <: and <=: perhaps. etc

[robin-aws]

Also relevant: #53. If we're going to introduce tri-valued comparison functions, we may want to do that first before adding more ordering-related utilities.

[ajewellamz]

I want to disagree with "since char values are currently UTF-16 code units and therefore a naive lexicographic comparison will likely not be correct for most uses".
The most important thing is to be able to have any TotalOrdering on a string; much less important that it be human friendly.