law Heap.pop.push_new

bend-kit-collections@0.1.4.1 · heap.bend:109

import Base

109# LAW: popping what was pushed onto an empty heap gives it back
110law Heap.pop.push_new:
111  for -x: U32
112  {Heap.pop(~U32, ~U32.is_le, Heap.push(~U32, ~U32.is_le, x, Heap.new(U32)))
113   == Some{(x, Heap.new(U32))} : Maybe<&1, U32 & Heap<U32>>}