def off.len_drop

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

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

916def off.len_drop(+n: Nat, ws: List<&2, B.OctByte>) -> {List.length(&2, B.OctByte, B.w8s.drop(n, ws)) == Nat.sub(List.length(&2, B.OctByte, ws), n) : Nat}:
917  match n ws:
918    case 0n Nil{}:
919      {==}
920    case 0n Con{x, t}:
921      {==}
922    case 1n+p Nil{}:
923      {==}
924    case 1n+p Con{x, t}:
925      off.len_drop(p, t)