Dafny restriction to ordered types
12:16 04 Jan 2026

I'm working with Dafny types which are totally ordered by <=, i.e. int and real (and ORDINAL). I want to minimize the redundant logic I write using their orders. For this post, I'll use the median function as an example. If I want to compute medians for sequences of ints and reals, I could write duplicate functions which are identical except for their signatures:

function MedianInt(s: seq): int
...
function MedianReal(s: seq): real
...

One would hope to avoid such code duplication with a template. But here there is no trait extended by both int and real, and no syntactic sugar like T(<=) for totally ordered types. Is there a way?

dafny