def p_at_list

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

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

1237def p_at_list(+o: B.Octets, +i: Nat) -> {B.Octets.at(o, i) == B.at(B.Octets.to_list(o), i) : Maybe<&2, U32>}:
1238  match o:
1239    case B.Octets{+ws}:
1240      %F_to(ws) : {B.w8s.at(B.w8s.drop(i, ws)) == B.at(_, i) : Maybe<&2, U32>}
1241      off.at_to(i, ws)