def bxor_comm

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/gf.bend:21

import Base

21def bxor_comm(+a: Bool, +b: Bool) -> {Bool.xor(a, b) == Bool.xor(b, a) : Bool}:
22  match a b:
23    case True{} True{}:
24      {==}
25    case True{} False{}:
26      {==}
27    case False{} True{}:
28      {==}
29    case False{} False{}:
30      {==}