law map_append

bend-mathlib@0.8.1.0 · list.bend:194

import Base

194# Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys.
195law map_append:
196  for ~A: Type
197  for ~B: Type
198  for ~f: A -> B
199  for xs: List<A>
200  for -ys: List<A>
201  {List.map(~A, ~B, ~f, List.append(&1, A, xs, ys)) == List.append(&1, B, List.map(~A, ~B, ~f, xs), List.map(~A, ~B, ~f, ys)) : List<B>}