def off.llen_be32

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

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

1050def off.llen_be32(+v: U32) -> {B.len(B.be32(v)) == 4n : Nat}:
1051  match v:
1052    case U32{w}:
1053      {==}