def off.add_be32

bend-osdev-bytes@0.1.1.0 · PROOF.bend:1070

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B

1070def off.add_be32(+x: U32, +y: U32) -> {Nat.add(B.len(B.be32(x)), B.len(B.be32(y))) == 8n : Nat}:
1071  match x y:
1072    case U32{a} U32{b}:
1073      {==}