def off.at_to

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

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

976def off.at_to(+i: Nat, ws: List<&2, B.OctByte>) -> {B.w8s.at(B.w8s.drop(i, ws)) == B.at(B.w8s.to_list(ws), i) : Maybe<&2, U32>}:
977  match i ws:
978    case 0n Nil{}:
979      {==}
980    case 1n+p Nil{}:
981      {==}
982    case 0n Con{B.OctByte{a0, a1, a2, a3, a4, a5, a6, a7}, t}:
983      {==}
984    case 1n+p Con{x, t}:
985      off.at_to(p, t)