law maybe_bind_pure_sym

bend-mathlib@0.8.1.0 · maybe.bend:236

import Base

236# Right identity: binding pure is the identity, reversed to rewrite toward the simple side.
237law maybe_bind_pure_sym:
238  for ~A: Data
239  for m: Maybe<&2, A>
240  {m == Maybe.bind(&2, A, A, m, x => Maybe.pure(&2, A, x)) : Maybe<&2, A>}