law maybe_or_none_sym

bend-mathlib@0.8.1.0 · maybe.bend:346

import Base

346# None is a right identity for or, reversed to rewrite toward the simple side.
347law maybe_or_none_sym:
348  for ~A: Data
349  for m: Maybe<&2, A>
350  {m == Maybe.or(&2, A, m, None{}) : Maybe<&2, A>}