def off.llen_le16

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

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

1055def off.llen_le16(+v: U32) -> {B.len(B.le16(v)) == 2n : Nat}:
1056  match v:
1057    case U32{w}:
1058      {==}