def off.llen_be16

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

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

1060def off.llen_be16(+v: U32) -> {B.len(B.be16(v)) == 2n : Nat}:
1061  match v:
1062    case U32{w}:
1063      {==}