def pk.bb

bend-osdev-pkcs7@0.1.0.0 · PROOF.bend:202

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

202# BEGIN GENERATED by gen/pkcs7_proof.py: bits
203# a byte's byte is itself
204def pk.bb(u: U32) -> {B.byte(B.byte(u)) == B.byte(u) : U32}:
205  match u:
206    case U32{WCon{u0, WCon{u1, WCon{u2, WCon{u3, WCon{u4, WCon{u5, WCon{u6, WCon{u7, WCon{u8, WCon{u9, WCon{u10, WCon{u11, WCon{u12, WCon{u13, WCon{u14, WCon{u15, WCon{u16, WCon{u17, WCon{u18, WCon{u19, WCon{u20, WCon{u21, WCon{u22, WCon{u23, WCon{u24, WCon{u25, WCon{u26, WCon{u27, WCon{u28, WCon{u29, WCon{u30, WCon{u31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
207      {==}