law pop_model

bend-lawful-stdlib@0.1.0.0 · src/queue.bend:84

import Base
import bend-lawful-stdlib@0.1.0.0/src/list.bend as List

84# pop returns the model's head and tail.
85law pop_model:
86  for -A: Data
87  for q: Queue<A>
88  {List.uncons(A, model(A, q)) == pop.model(A, pop(A, q)) : List.Step<&2, A, List<&2, A>>}