law maybe_bind_assoc

bend-mathlib@0.8.1.0 · maybe.bend:28

import Base

28# Bind is associative.
29law maybe_bind_assoc:
30  for ~A: Data
31  for ~B: Data
32  for ~C: Data
33  for -f: A -> Maybe<&2, B>
34  for -g: B -> Maybe<&2, C>
35  for m: Maybe<&2, A>
36  {Maybe.bind(&2, B, C, Maybe.bind(&2, A, B, m, f), g) == Maybe.bind(&2, A, C, m, x => Maybe.bind(&2, B, C, f(x), g)) : Maybe<&2, C>}