chickadee » random-access-lists » ral-clear!

command ((oldcount newcount ral-count) (oldheight newheight ral-height))
requires (ral? ls)
ensures  (and (fx= 0 newcount) (fx= 1 newheight))