law maybe_or_none

bend-mathlib@0.8.1.0 · maybe.bend:161

import Base

161# None is a right identity for or.
162law maybe_or_none:
163  for ~A: Data
164  for m: Maybe<&2, A>
165  {Maybe.or(&2, A, m, None{}) == m : Maybe<&2, A>}