PROOF.pk_rt: def of bend-osdev-acpi@0.1.1.0
Import: import bend-osdev-acpi@0.1.1.0/PROOF.bend as PROOF
Lines 162-165 of bend-osdev-acpi@0.1.1.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&start_line=162&end_line=165

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-acpi@0.1.1.0/error.bend as E
import bend-osdev-acpi@0.1.1.0/aml_pkglength.bend as K

def pk_rt(+v: U32, +r: List<&2, U32>, +fits: {K.AmlPkgLength.fits(v) == True{} : Bool}) -> {K.pk.pub(K.pk.dec(B.append(B.mask(K.pk.enc(v)), r))) == Done{K.AmlPkgLen{v, B.Octets.of_list(r)}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}:
  match v:
    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
      pk_bits(b31, b30, b29, b28, b27, b26, b25, b24, b23, b22, b21, b20, b19, b18, b17, b16, b15, b14, b13, b12, b11, b10, b9, b8, b7, b6, b5, b4, b3, b2, b1, b0, r, fits)

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=pk_bits
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_pkglength.bend&name=AmlPkgLen
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_pkglength.bend&name=AmlPkgLength.fits
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_pkglength.bend&name=pk.dec
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_pkglength.bend&name=pk.enc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_pkglength.bend&name=pk.pub
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/error.bend&name=AcpiError
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=mask