val serialize32_asn1_generalized_time_TLV_backwards
: serializer32_backwards (serialize_asn1_generalized_time_TLV)
val serialize32_asn1_generalized_time_TLV_backwards
: serializer32_backwards (serialize_asn1_generalized_time_TLV)
let serialize32_asn1_generalized_time_TLV_backwards
= serialize32_tagged_union_backwards
  (* st32 *) (serialize32_asn1_tag_of_type_backwards Generalized_Time
              `serialize32_nondep_then_backwards`
              serialize32_asn1_length_of_type_backwards Generalized_Time)
  (* tg32 *) (parser_tag_of_generalized_time)
  (* sd32 *) (fun tag -> serialize32_synth_backwards
                         (serialize32_asn1_generalized_time_backwards)
                         (synth_asn1_oid_V tag)
                         (synth_asn1_oid_V_inverse tag)
                         (synth_asn1_oid_V_inverse tag)
                         ())
module ASN1.Low.Value.Generalized_Time

open ASN1.Low.Base

open ASN1.Base
open ASN1.Low.Tag
open ASN1.Low.Length
open ASN1.Low.Bytes32
open ASN1.Spec.Value.Generalized_Time

open FStar.Integers

module B32 = FStar.Bytes

friend ASN1.Spec.Value.Generalized_Time

#set-options "--fuel 0 --ifuel 2"

let serialize32_asn1_generalized_time_backwards
= serialize32_flbytes32_backwards 15ul
  `serialize32_filter_backwards`
  valid_generalized_time
/
prims.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.Value.Generalized_Time.fst.checked ASN1.Spec.Value.Generalized_Time.fst.checked ASN1.Low.Tag.fsti.checked ASN1.Low.Length.fsti.checked ASN1.Low.Bytes32.fst.checked ASN1.Low.Base.fst.checked ASN1.Base.fst.checked
ASN1.Low.Value.Generalized_Time.fst
ASN1.Low.Base.serializer32_backwards ASN1.Spec.Value.Generalized_Time.serialize_asn1_generalized_time_TLV

ASN1.Low.Base.serialize32_tagged_union_backwards 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 FStar.Pervasives.Native.tuple2 ASN1.Base.the_asn1_tag ASN1.Base.asn1_value_int32_of_type LowParse.Spec.Combinators.nondep_then ASN1.Spec.Tag.parse_asn1_tag_of_type ASN1.Spec.Length.parse_asn1_length_of_type LowParse.Spec.Combinators.serialize_nondep_then ASN1.Spec.Tag.serialize_asn1_tag_of_type ASN1.Spec.Length.serialize_asn1_length_of_type ASN1.Low.Base.serialize32_nondep_then_backwards ASN1.Low.Tag.serialize32_asn1_tag_of_type_backwards ASN1.Low.Length.serialize32_asn1_length_of_type_backwards ASN1.Base.datatype_of_asn1_type ASN1.Spec.Value.Generalized_Time.parser_tag_of_generalized_time ASN1.Spec.Value.Generalized_Time.parse_asn1_generalized_time_kind LowParse.Spec.Combinators.parse_synth LowParse.Spec.Base.refine_with_tag ASN1.Spec.Value.Generalized_Time.parse_asn1_generalized_time ASN1.Spec.Value.Generalized_Time.synth_asn1_oid_V LowParse.Spec.Base.parser LowParse.Spec.Combinators.serialize_synth ASN1.Spec.Value.Generalized_Time.serialize_asn1_generalized_time ASN1.Spec.Value.Generalized_Time.synth_asn1_oid_V_inverse LowParse.Spec.Base.serializer ASN1.Low.Base.serialize32_synth_backwards ASN1.Low.Value.Generalized_Time.serialize32_asn1_generalized_time_backwards ASN1.Low.Base.serializer32_backwards
let serialize32_asn1_generalized_time_TLV_backwards =
  
serialize32_tagged_union_backwards ((serialize32_asn1_tag_of_type_backwards Generalized_Time)
    `serialize32_nondep_then_backwards`
    (serialize32_asn1_length_of_type_backwards Generalized_Time))
  (parser_tag_of_generalized_time)
  (fun tag ->
      serialize32_synth_backwards (serialize32_asn1_generalized_time_backwards)
        (synth_asn1_oid_V tag)
        (synth_asn1_oid_V_inverse tag)
        (synth_asn1_oid_V_inverse tag)
        ())