law maybe_bind_none

bend-mathlib@0.8.1.0 · maybe.bend:86

import Base

86# Binding a function that always fails gives None.
87law maybe_bind_none:
88  for ~A: Data
89  for ~B: Data
90  for m: Maybe<&2, A>
91  {Maybe.bind(&2, A, B, m, x => None{}) == None{} : Maybe<&2, B>}