dafny-lang / libraries

Libraries useful for Dafny programs
Other
43 stars 25 forks source link

Request: support for comparison functions that return a {less than, equal, greater than} result #53

Open robin-aws opened 1 year ago

robin-aws commented 1 year ago

Another spinoff from #49, which was de-scoped to use plain (T, T) -> bool predicates instead. A tri-valued comparison function tends to be more general and saves on the number of comparisons necessary in many algorithms.

We have a bunch of code from the compiler-bootstrap project that we can borrow from on this: https://github.com/dafny-lang/compiler-bootstrap/blob/28299a21101342e5384664c71103c562ad707a80/src/Utils/Library.dfy#L670