law maybe_bind_map

bend-mathlib@0.8.1.0 · maybe.bend:189

import Base

189# Binding after a map binds the composition.
190law maybe_bind_map:
191  for ~A: Data
192  for ~B: Data
193  for ~C: Data
194  for ~f: A -> B
195  for ~g: B -> Maybe<&2, C>
196  for m: Maybe<&2, A>
197  {Maybe.bind(&2, B, C, Maybe.map(&2, A, B, f, m), g) == Maybe.bind(&2, A, C, m, x => g(f(x))) : Maybe<&2, C>}