law Deque.lemma.reverse_go

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

import Base

252# reversing onto an accumulator is reversing, then appending it
253law Deque.lemma.reverse_go:
254  for -A: Data
255  for  xs: List<&2, A>
256  for -acc: List<&2, A>
257  {List.append(&2, A, List.reverse.go(&2, A, xs, Nil{}), acc)
258   == List.reverse.go(&2, A, xs, acc) : List<&2, A>}