def off.at_take

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

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

961def off.at_take(+i: Nat, +n: Nat, ws: List<&2, B.OctByte>) -> {Nat.is_lt(i, n) == True{} : Bool} -> {B.w8s.at(B.w8s.drop(i, B.w8s.take(n, ws))) == B.w8s.at(B.w8s.drop(i, ws)) : Maybe<&2, U32>}:
962  match i n ws:
963    case 0n 0n _:
964      h => off.no({B.w8s.at(Nil{}) == B.w8s.at(ws) : Maybe<&2, U32>}, h)
965    case 1n+p 0n _:
966      h => off.no({B.w8s.at(B.w8s.drop(1n+p, Nil{})) == B.w8s.at(B.w8s.drop(1n+p, ws)) : Maybe<&2, U32>}, h)
967    case 0n 1n+q Nil{}:
968      h => {==}
969    case 0n 1n+q Con{x, t}:
970      h => {==}
971    case 1n+p 1n+q Nil{}:
972      h => {==}
973    case 1n+p 1n+q Con{x, t}:
974      h => off.at_take(p, q, t, h)