law maybe_map_bind

bend-mathlib@0.8.1.0 · maybe.bend:206

import Base

206# Mapping after a bind maps inside the bound function.
207law maybe_map_bind:
208  for ~A: Data
209  for ~B: Data
210  for ~C: Data
211  for ~f: A -> Maybe<&2, B>
212  for ~g: B -> C
213  for m: Maybe<&2, A>
214  {Maybe.map(&2, B, C, g, Maybe.bind(&2, A, B, m, f)) == Maybe.bind(&2, A, C, m, x => Maybe.map(&2, B, C, g, f(x))) : Maybe<&2, C>}