law maybe_pure_bind_sym

bend-mathlib@0.8.1.0 · maybe.bend:225

import Base

225# Left identity: binding a pure value applies the function, reversed to rewrite toward the simple side.
226law maybe_pure_bind_sym:
227  for ~A: Data
228  for ~B: Data
229  for -f: A -> Maybe<&2, B>
230  for -x: A
231  {f(x) == Maybe.bind(&2, A, B, Maybe.pure(&2, A, x), f) : Maybe<&2, B>}