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

command ((oldcount newcount (lambda (ls place item) (ral-count ls)))
         (olditem newitem (lambda (ls place item) (ral-ref ls place))))
requires (and (ral? ls) ((ral-item? ls) item)
              (fixnum? place) (fx>= place 0) (fx<= place (ral-count ls)))
ensures  (and (fx= newcount (fx+ 1 oldcount)) (equal? newitem item))