law Heap.size.push

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

import Base

118# LAW: a push adds one to the size
119law Heap.size.push:
120  for -x: U32
121  for  h: Heap<U32>
122  {Heap.size(U32, Heap.push(~U32, ~U32.is_le, x, h))
123   == 1n+Heap.size(U32, h) : Nat}