def or_bits

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64add.bend:129

import Base

129def or_bits(+c2: Bool, +c3: Bool) -> {Bool.or(c2, c3) == Bool.not(Nat.is_eq(Nat.add(bv(c3), bv(c2)), 0n)) : Bool}:
130  match c2 c3:
131    case True{} True{}:
132      {==}
133    case True{} False{}:
134      {==}
135    case False{} True{}:
136      {==}
137    case False{} False{}:
138      {==}