def off.add_le32

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

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

1065def off.add_le32(+x: U32, +y: U32) -> {Nat.add(B.len(B.le32(x)), B.len(B.le32(y))) == 8n : Nat}:
1066  match x y:
1067    case U32{a} U32{b}:
1068      {==}