Open robin-aws opened 1 year ago
We already kind of have ordered sets because of definitions like https://github.com/dafny-lang/libraries/blob/master/src/Collections/Sequences/Seq.dfy#L182. In both cases it would be very nice to provide subset types for these concepts.
Can you specify what you mean by an ordered map? Are you saying both domain and codomain have a partial order, and if x <= y, then m[x] <= m[y]?
x <= y
m[x] <= m[y]
We already kind of have ordered sets because of definitions like https://github.com/dafny-lang/libraries/blob/master/src/Collections/Sequences/Seq.dfy#L182. In both cases it would be very nice to provide subset types for these concepts.