val serialize_nlist
  (n: nat)
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p { k.parser_kind_subkind == Some ParserStrong } )
: Tot (y: serializer (parse_nlist n p) { y == serialize_nlist' n s })
let serialize_nlist
  (n: nat)
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p { k.parser_kind_subkind == Some ParserStrong } )
: Tot (y: serializer (parse_nlist n p) { y == serialize_nlist' n s })
= serialize_nlist' n s
val serialize_nlist
  (n: nat)
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p { k.parser_kind_subkind == Some ParserStrong } )
: Tot (y: serializer (parse_nlist n p) { y == serialize_nlist' n s })
let serialize_nlist
      (n: nat)
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p {k.parser_kind_subkind == Some ParserStrong})
    : Tot (y: serializer (parse_nlist n p) {y == serialize_nlist' n s}) =
serialize_nlist' n s
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.Base.serializer Prims.eq2 FStar.Pervasives.Native.option LowParse.Spec.Base.parser_subkind LowParse.Spec.Base.__proj__Mkparser_kind'__item__parser_kind_subkind FStar.Pervasives.Native.Some LowParse.Spec.Base.ParserStrong LowParse.Spec.VCList.serialize_nlist' LowParse.Spec.VCList.parse_nlist_kind LowParse.Spec.VCList.nlist LowParse.Spec.VCList.parse_nlist
(* 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)
: Tot (y: parser (parse_nlist_kind n k) (nlist n t) { y == parse_nlist' n p } )
= parse_nlist' n p

let serialize_nlist
  (n: nat)
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p { k.parser_kind_subkind == Some ParserStrong } )
val serialize_nlist
  (n: nat)
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p { k.parser_kind_subkind == Some ParserStrong } )
: Tot (y: serializer (parse_nlist n p) { y == serialize_nlist' n s })

    n: Prims.nat ->
    s:
      LowParse.Spec.Base.serializer p
        { Mkparser_kind'?.parser_kind_subkind k ==
          FStar.Pervasives.Native.Some LowParse.Spec.Base.ParserStrong }
  -> y:
    LowParse.Spec.Base.serializer (LowParse.Spec.VCList.parse_nlist n p)
      {y == LowParse.Spec.VCList.serialize_nlist' n s}