law maybe_map_eq_bind_sym

bend-mathlib@0.8.1.0 · maybe.bend:301

import Base

301# Mapping is binding the function followed by pure, reversed to rewrite toward the simple side.
302law maybe_map_eq_bind_sym:
303  for ~A: Data
304  for ~B: Data
305  for ~f: A -> B
306  for m: Maybe<&2, A>
307  {Maybe.bind(&2, A, B, m, x => Maybe.pure(&2, B, f(x))) == Maybe.map(&2, A, B, f, m) : Maybe<&2, B>}