law map_reverse

bend-mathlib@0.8.1.0 · list.bend:521

import Base

521# Mapping commutes with reversing: map f (reverse xs) = reverse (map f xs).
522law map_reverse:
523  for ~A: Type
524  for ~B: Type
525  for ~f: A -> B
526  for xs: List<A>
527  {List.map(~A, ~B, ~f, List.reverse(&1, A, xs)) == List.reverse(&1, B, List.map(~A, ~B, ~f, xs)) : List<B>}