law maybe_map_eq_bind

bend-mathlib@0.8.1.0 · maybe.bend:100

import Base

100# Mapping is binding the function followed by pure.
101law maybe_map_eq_bind:
102  for ~A: Data
103  for ~B: Data
104  for ~f: A -> B
105  for m: Maybe<&2, A>
106  {Maybe.map(&2, A, B, f, m) == Maybe.bind(&2, A, B, m, x => Maybe.pure(&2, B, f(x))) : Maybe<&2, B>}