val parse_nlist_tailrec
      (n: nat)
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (accu: (list t * nat))
      (b: bytes)
    : GTot (option (list t * nat))
let rec parse_nlist_tailrec
  (n: nat)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (accu: list t * nat)
  (b: bytes)
: GTot (option (list t * nat))
= if n = 0
  then Some accu
  else
    match parse p b with
    | Some (elem, consumed) ->
      let (l0, consumed0) = accu in
      let b' = Seq.slice b consumed (Seq.length b) in
      parse_nlist_tailrec (n - 1) p (elem :: l0, consumed0 + consumed) b'
    | _ -> None
val parse_nlist_tailrec
      (n: nat)
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (accu: (list t * nat))
      (b: bytes)
    : GTot (option (list t * nat))
let rec parse_nlist_tailrec
      (n: nat)
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (accu: list t * nat)
      (b: bytes)
    : GTot (option (list t * nat)) =
if n = 0
then Some accu
else
  match parse p b with
  | Some (elem, consumed) ->
    let l0, consumed0 = accu in
    let b' = Seq.slice b consumed (Seq.length b) in
    parse_nlist_tailrec (n - 1) p (elem :: l0, consumed0 + consumed) b'
  | _ -> None
LowParse.SLow.VCList.fst.checked
prims.fst.checked LowParse.Spec.VCList.fsti.checked LowParse.SLow.List.fst.checked LowParse.Math.fst.checked LowParse.Bytes32.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked C.Loops.fst.checked
LowParse.SLow.VCList.fst
Prims.nat LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser FStar.Pervasives.Native.tuple2 Prims.list LowParse.Bytes.bytes Prims.op_Equality Prims.int FStar.Pervasives.Native.Some Prims.bool LowParse.Spec.Base.parse LowParse.Spec.Base.consumed_length LowParse.SLow.VCList.parse_nlist_tailrec Prims.op_Subtraction FStar.Pervasives.Native.Mktuple2 Prims.Cons Prims.op_Addition FStar.Seq.Base.seq LowParse.Bytes.byte FStar.Seq.Base.slice FStar.Seq.Base.length FStar.Pervasives.Native.option FStar.Pervasives.Native.None
module LowParse.SLow.VCList
include LowParse.Spec.VCList
include LowParse.SLow.List

module Seq = FStar.Seq
module U32 = FStar.UInt32
module Classical = FStar.Classical
module L = FStar.List.Tot
module B32 = LowParse.Bytes32

let rec parse_nlist_tailrec
  (n: nat)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (accu: list t * nat)
  (b: bytes)
val parse_nlist_tailrec
      (n: nat)
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (accu: (list t * nat))
      (b: bytes)
    : GTot (option (list t * nat))

    n: Prims.nat ->
    p: LowParse.Spec.Base.parser k t ->
    accu: (Prims.list t * Prims.nat) ->
    b: LowParse.Bytes.bytes
  -> Prims.GTot (FStar.Pervasives.Native.option (Prims.list t * Prims.nat))