def bits8_of_bits8

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

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

146def bits8_of_bits8(w: B.OctByte) -> {B.oct.of(B.oct.to(w)) == w : B.OctByte}:
147  match w:
148    case B.OctByte{a0, a1, a2, a3, a4, a5, a6, a7}:
149      {==}