law maybe_pure_bind

bend-mathlib@0.8.1.0 · maybe.bend:4

import Base

4# Left identity: binding a pure value applies the function.
5law maybe_pure_bind:
6  for ~A: Data
7  for ~B: Data
8  for -f: A -> Maybe<&2, B>
9  for -x: A
10  {Maybe.bind(&2, A, B, Maybe.pure(&2, A, x), f) == f(x) : Maybe<&2, B>}