law maybe_bind_pure

bend-mathlib@0.8.1.0 · maybe.bend:15

import Base

15# Right identity: binding pure is the identity.
16law maybe_bind_pure:
17  for ~A: Data
18  for m: Maybe<&2, A>
19  {Maybe.bind(&2, A, A, m, x => Maybe.pure(&2, A, x)) == m : Maybe<&2, A>}