law push_model

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

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

55# push appends x to the model.
56law push_model:
57  for -A: Data
58  for q: Queue<A>
59  for +x: A
60  {List.append(&2, A, model(A, q), [x]) == model(A, push(A, q, x)) : List<&2, A>}