val parse_nlist
  (n: nat)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Tot (y: parser (parse_nlist_kind n k) (nlist n t) { y == parse_nlist' n p } )
let parse_nlist
  (n: nat)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Tot (y: parser (parse_nlist_kind n k) (nlist n t) { y == parse_nlist' n p } )
= parse_nlist' n p
val parse_nlist
  (n: nat)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Tot (y: parser (parse_nlist_kind n k) (nlist n t) { y == parse_nlist' n p } )
let parse_nlist (n: nat) (#k: parser_kind) (#t: Type) (p: parser k t)
    : Tot (y: parser (parse_nlist_kind n k) (nlist n t) {y == parse_nlist' n p}) =
parse_nlist' n p
LowParse.Spec.VCList.fst.checked
prims.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.Array.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
LowParse.Spec.VCList.fst
Prims.nat LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.VCList.parse_nlist' LowParse.Spec.VCList.parse_nlist_kind LowParse.Spec.VCList.nlist Prims.eq2
(* Variable-count lists *)

module LowParse.Spec.VCList
include LowParse.Spec.Combinators // for seq_slice_append_l
include LowParse.Spec.Array // for vlarray

module Seq = FStar.Seq
module U32 = FStar.UInt32
module Classical = FStar.Classical
module L = FStar.List.Tot

let parse_nlist
  (n: nat)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
val parse_nlist
  (n: nat)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Tot (y: parser (parse_nlist_kind n k) (nlist n t) { y == parse_nlist' n p } )
n: Prims.nat -> p: LowParse.Spec.Base.parser k t
  -> y:
    LowParse.Spec.Base.parser (LowParse.Spec.VCList.parse_nlist_kind n k)
      (LowParse.Spec.VCList.nlist n t) {y == LowParse.Spec.VCList.parse_nlist' n p}