val 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 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)
val 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 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)
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
Prims.bool Prims.nat Prims.dtuple2 LowParse.Spec.ListUpTo.parse_list_up_to_payload_t FStar.Pervasives.Native.Mktuple2 LowParse.Spec.ListUpTo.llist LowParse.Spec.ListUpTo.refine_with_cond LowParse.Spec.ListUpTo.negate_cond Prims.op_Addition Prims.Nil Prims.Cons LowParse.Spec.ListUpTo.parse_list_up_to_fuel_t
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))
val 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))

    cond: (_: t -> Prims.bool) ->
    fuel: Prims.nat ->
    xy: Prims.dtuple2 t (LowParse.Spec.ListUpTo.parse_list_up_to_payload_t cond fuel)
  -> LowParse.Spec.ListUpTo.parse_list_up_to_fuel_t cond (fuel + 1)