val parse_seq_all_bytes' (input: bytes) : GTot (option (bytes * consumed_length input))
val parse_seq_all_bytes' (input: bytes) : GTot (option (bytes * consumed_length input))
let parse_seq_all_bytes'
  (input: bytes)
: GTot (option (bytes * consumed_length input))
= let len = Seq.length input in
    Some (input, len)
module LowParse.Spec.SeqBytes
include LowParse.Spec.SeqBytes.Base
include LowParse.Spec.VLData

module Seq = FStar.Seq
module U32 = FStar.UInt32

(* VLBytes *)

(* For the payload: since the input buffer is truncated at the time of
reading the length header, "parsing" the payload will always succeed,
by just returning it unchanged (unless the length of the input
is greater than 2^32) *)

let parse_seq_all_bytes_kind =
  {
    parser_kind_low = 0;
    parser_kind_high = None;
    parser_kind_metadata = None;
    parser_kind_subkind = Some ParserConsumesAll;
  }
/
prims.fst.checked LowParse.Spec.VLData.fsti.checked LowParse.Spec.SeqBytes.Base.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.SeqBytes.fst
input: LowParse.Bytes.bytes
  -> Prims.GTot
    (FStar.Pervasives.Native.option (LowParse.Bytes.bytes * LowParse.Spec.Base.consumed_length input
        ))
LowParse.Bytes.bytes FStar.Pervasives.Native.Some FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.consumed_length FStar.Pervasives.Native.Mktuple2 Prims.nat FStar.Seq.Base.length LowParse.Bytes.byte FStar.Pervasives.Native.option
let parse_seq_all_bytes' (input: bytes) : GTot (option (bytes * consumed_length input)) =
  
let len = Seq.length input in
Some (input, len)