law Deque.to_list.push_front

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

import Base

171# LAW: push_front puts the element at the head of the list
172law Deque.to_list.push_front:
173  for -A: Data
174  for -x: A
175  for  d: Deque<&2, A>
176  {Deque.to_list(&2, A, Deque.push_front(&2, A, x, d))
177   == x <> Deque.to_list(&2, A, d) : List<&2, A>}