law maybe_or_assoc_sym

bend-mathlib@0.8.1.0 · maybe.bend:355

import Base

355# Or is associative, reversed to rewrite toward the simple side.
356law maybe_or_assoc_sym:
357  for ~A: Data
358  for m: Maybe<&2, A>
359  for -n: Maybe<&2, A>
360  for -k: Maybe<&2, A>
361  {Maybe.or(&2, A, m, Maybe.or(&2, A, n, k)) == Maybe.or(&2, A, Maybe.or(&2, A, m, n), k) : Maybe<&2, A>}