law maybe_or_assoc

bend-mathlib@0.8.1.0 · maybe.bend:174

import Base

174# Or is associative.
175law maybe_or_assoc:
176  for ~A: Data
177  for m: Maybe<&2, A>
178  for -n: Maybe<&2, A>
179  for -k: Maybe<&2, A>
180  {Maybe.or(&2, A, Maybe.or(&2, A, m, n), k) == Maybe.or(&2, A, m, Maybe.or(&2, A, n, k)) : Maybe<&2, A>}