def off.at_app_lt

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

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

950def off.at_app_lt(+i: Nat, xs: List<&2, B.OctByte>, +ys: List<&2, B.OctByte>) -> {Nat.is_lt(i, List.length(&2, B.OctByte, xs)) == True{} : Bool} -> {B.w8s.at(B.w8s.drop(i, List.append(&2, B.OctByte, xs, ys))) == B.w8s.at(B.w8s.drop(i, xs)) : Maybe<&2, U32>}:
951  match i xs:
952    case 0n Nil{}:
953      h => off.no({B.w8s.at(ys) == None{} : Maybe<&2, U32>}, h)
954    case 1n+p Nil{}:
955      h => off.no({B.w8s.at(B.w8s.drop(1n+p, ys)) == None{} : Maybe<&2, U32>}, h)
956    case 0n Con{x, t}:
957      h => {==}
958    case 1n+p Con{x, t}:
959      h => off.at_app_lt(p, t, ys, h)