def pk.drop_fill

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

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

195def pk.drop_fill(+k: Nat, +v: U32) -> {B.drop(k, P.pkcs7.fill(1n+k, v)) == Con{v, Nil{}} : List<&2, U32>}:
196  match k:
197    case 0n:
198      {==}
199    case 1n+kp:
200      pk.drop_fill(kp, v)