law maybe_map_bind_sym

bend-mathlib@0.8.1.0 · maybe.bend:379

import Base

379# Mapping after a bind maps inside the bound function, reversed to rewrite toward the simple side.
380law maybe_map_bind_sym:
381  for ~A: Data
382  for ~B: Data
383  for ~C: Data
384  for ~f: A -> Maybe<&2, B>
385  for ~g: B -> C
386  for m: Maybe<&2, A>
387  {Maybe.bind(&2, A, C, m, x => Maybe.map(&2, B, C, g, f(x))) == Maybe.map(&2, B, C, g, Maybe.bind(&2, A, B, m, f)) : Maybe<&2, C>}