)abbrev Domain ORDKE OrderedKeyEntry
OrderedKeyEntry(Key:OrderedSet,Entry:SetCategory): Exports == Implementation where
  Exports == OrderedSet with
    construct: (Key,Entry) -> %
    elt: (%,"key") -> Key
    elt: (%,"entry") -> Entry
  Implementation == add
    Rep := Record(k:Key,e:Entry)
    x,y: %
    construct(a,b) == construct(a,b)$Rep @ %
    elt(x,"key"):Key == (x@Rep).k
    elt(x,"entry"):Entry == (x@Rep).e
    x < y == x.key < y.key
    x = y == x.key = y.key
    hash x == hash(x.key)
    if Entry has CoercibleTo OutputForm then
      coerce(x):OutputForm == bracket [(x.key)::OutputForm,(x.entry)::OutputForm]
)abbrev Domain PRIORITY PriorityQueue
S ==> OrderedKeyEntry(Key,Entry)
PriorityQueue(Key:OrderedSet,Entry:SetCategory): Exports == Implementation where
  Exports == PriorityQueueAggregate S with
    heap : List S  -> %
    setelt: (%,Key,Entry) -> Entry
  Implementation == Heap(S) add
    setelt(x:%,key:Key,entry:Entry) ==
      insert!(construct(key,entry)$S,x)
      entry