val parse_asn1_generalized_time_TLV_kind:parser_kind
val parse_asn1_generalized_time_TLV_kind:parser_kind
let parse_asn1_generalized_time_TLV_kind
: parser_kind
= parse_asn1_tag_kind
  `and_then_kind`
  parse_asn1_length_kind_of_type Generalized_Time
  `and_then_kind`
  parse_asn1_generalized_time_kind
module ASN1.Spec.Value.Generalized_Time

open ASN1.Spec.Base

open ASN1.Base
open ASN1.Spec.Tag
open ASN1.Spec.Length
open ASN1.Spec.Bytes32

open FStar.Integers

module B32 = FStar.Bytes

#set-options "--z3rlimit 32  --fuel 0 --ifuel 0"

inline_for_extraction noextract
let parse_asn1_generalized_time_kind: parser_kind
= parse_filter_kind (total_constant_size_parser_kind 15)

val parse_asn1_generalized_time
: parser parse_asn1_generalized_time_kind (datatype_of_asn1_type Generalized_Time)

val serialize_asn1_generalized_time
: serializer (parse_asn1_generalized_time)
/
prims.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Spec.Bytes32.fst.checked ASN1.Spec.Base.fst.checked ASN1.Base.fst.checked
ASN1.Spec.Value.Generalized_Time.fsti
LowParse.Spec.Base.parser_kind
LowParse.Spec.Combinators.and_then_kind ASN1.Spec.Tag.parse_asn1_tag_kind ASN1.Spec.Length.parse_asn1_length_kind_of_type ASN1.Base.Generalized_Time ASN1.Spec.Value.Generalized_Time.parse_asn1_generalized_time_kind
let parse_asn1_generalized_time_TLV_kind:parser_kind =
  
(parse_asn1_tag_kind `and_then_kind` (parse_asn1_length_kind_of_type Generalized_Time))
`and_then_kind`
parse_asn1_generalized_time_kind