law Deque.pop_front.push_front

bend-kit-collections@0.1.4.1 · deque.bend:184

import Base

184# LAW: pop_front undoes push_front
185law Deque.pop_front.push_front:
186  for -A: Data
187  for -x: A
188  for  d: Deque<&2, A>
189  {Deque.pop_front(&2, A, Deque.push_front(&2, A, x, d))
190   == Some{(x, d)} : Maybe<&1, A & Deque<&2, A>>}