law reverse_go_spec

bend-mathlib@0.8.1.0 · list.bend:72

import Base

72# The reverse accumulator loop appends the reversed list to the accumulator.
73law reverse_go_spec:
74  for -a: Quant
75  for -A: Kind(a)
76  for xs: List<a, A>
77  for -acc: List<a, A>
78  {List.reverse.go(a, A, xs, acc) == List.append(a, A, List.reverse(a, A, xs), acc) : List<a, A>}