val parse_list_up_to_payload_kind (k: parser_kind) : Tot (k': parser_kind{k' `is_weaker_than` k})
let parse_list_up_to_payload_kind (k: parser_kind) : Tot (k' : parser_kind {k' `is_weaker_than` k }) = {
  parser_kind_low = 0;
  parser_kind_high = None;
  parser_kind_subkind = k.parser_kind_subkind;
  parser_kind_metadata = None;
}
val parse_list_up_to_payload_kind (k: parser_kind) : Tot (k': parser_kind{k' `is_weaker_than` k})
let parse_list_up_to_payload_kind (k: parser_kind) : Tot (k': parser_kind{k' `is_weaker_than` k}) =
{
  parser_kind_low = 0;
  parser_kind_high = None;
  parser_kind_subkind = k.parser_kind_subkind;
  parser_kind_metadata = None
}
LowParse.Spec.ListUpTo.fst.checked
prims.fst.checked LowParse.Spec.Seq.fst.checked LowParse.Spec.Fuel.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.ListUpTo.fst
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.Mkparser_kind' FStar.Pervasives.Native.None Prims.nat LowParse.Spec.Base.__proj__Mkparser_kind'__item__parser_kind_subkind LowParse.Spec.Base.parser_kind_metadata_some LowParse.Spec.Base.is_weaker_than
module LowParse.Spec.ListUpTo
open LowParse.Spec.Base
open LowParse.Spec.Fuel
open LowParse.Spec.Combinators

let llist
  (t: Type)
  (fuel: nat)
: Tot Type
= (l: list t { L.length l < fuel })

let parse_list_up_to_fuel_t
  (#t: Type)
  (cond: (t -> Tot bool))
  (fuel: nat)
: Tot Type
= (llist (refine_with_cond (negate_cond cond)) fuel) & refine_with_cond cond

(* Universe-polymorphic unit type *)
type up_unit : Type u#r = | UP_UNIT

let parse_list_up_to_payload_t
  (#t: Type)
  (cond: (t -> Tot bool))
  (fuel: nat)
  (x: t)
: Tot Type
= if cond x
  then up_unit
  else parse_list_up_to_fuel_t cond fuel

let synth_list_up_to_fuel
  (#t: Type)
  (cond: (t -> Tot bool))
  (fuel: nat)
  (xy: dtuple2 t (parse_list_up_to_payload_t cond fuel))
: Tot (parse_list_up_to_fuel_t cond (fuel + 1))
= let (| x, yz |) = xy in
  if cond x
  then ([], x)
  else
    let (y, z) = (yz <: parse_list_up_to_fuel_t cond fuel) in
    (x :: y, z)

let synth_list_up_to_injective
  (#t: Type)
  (cond: (t -> Tot bool))
  (fuel: nat)
: Lemma
  (synth_injective (synth_list_up_to_fuel cond fuel))
  [SMTPat (synth_injective (synth_list_up_to_fuel cond fuel))]
= ()

inline_for_extraction
val parse_list_up_to_payload_kind (k: parser_kind) : Tot (k': parser_kind{k' `is_weaker_than` k})
k: LowParse.Spec.Base.parser_kind
  -> k': LowParse.Spec.Base.parser_kind{LowParse.Spec.Base.is_weaker_than k' k}