law reverse_go_spec_sym

bend-mathlib@0.8.1.0 · list.bend:2171

import Base

2171# The reverse accumulator loop appends the reversed list to the accumulator, reversed to rewrite toward the simple side.
2172law reverse_go_spec_sym:
2173  for -a: Quant
2174  for -A: Kind(a)
2175  for xs: List<a, A>
2176  for -acc: List<a, A>
2177  {List.append(a, A, List.reverse(a, A, xs), acc) == List.reverse.go(a, A, xs, acc) : List<a, A>}