law maybe_bind_none_sym

bend-mathlib@0.8.1.0 · maybe.bend:291

import Base

291# Binding a function that always fails gives None, reversed to rewrite toward the simple side.
292law maybe_bind_none_sym:
293  for ~A: Data
294  for ~B: Data
295  for m: Maybe<&2, A>
296  {None{} == Maybe.bind(&2, A, B, m, x => None{}) : Maybe<&2, B>}