def off.llen_le32

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

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

1045def off.llen_le32(+v: U32) -> {B.len(B.le32(v)) == 4n : Nat}:
1046  match v:
1047    case U32{w}:
1048      {==}