val parse_x509_extension_payload
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (oid: datatype_of_asn1_type OID)
  (s: serializer p)
: parser parse_x509_extension_payload_kind (x509_extension_payload_t oid s)
val parse_x509_extension_payload
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (oid: datatype_of_asn1_type OID)
  (s: serializer p)
: parser parse_x509_extension_payload_kind (x509_extension_payload_t oid s)
let parse_x509_extension_payload #k #t #p oid s
=
  parse_asn1_oid_TLV_of oid
  `nondep_then`
  parse_asn1_TLV_of_type BOOLEAN
  `nondep_then`
 (OCTET_STRING
  `parse_asn1_envelop_tag_with_TLV`
  s)
module X509.BasicFields.Extension2

open LowParse.Spec.Base
open LowParse.Spec.Combinators

open ASN1.Base
open ASN1.Spec
open ASN1.Low

open X509.Base

open FStar.Integers

module B32 = FStar.Bytes

#set-options "--z3rlimit 32 --fuel 0 --ifuel 0"
/
X509.Base.fst.checked prims.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.Base.fsti.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked ASN1.Base.fst.checked
X509.BasicFields.Extension2.fst
oid: ASN1.Base.datatype_of_asn1_type ASN1.Base.OID -> s: LowParse.Spec.Base.serializer p
  -> LowParse.Spec.Base.parser X509.BasicFields.Extension2.parse_x509_extension_payload_kind
      (X509.BasicFields.Extension2.x509_extension_payload_t oid (FStar.Ghost.hide s))
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser ASN1.Base.datatype_of_asn1_type ASN1.Base.OID LowParse.Spec.Base.serializer LowParse.Spec.Combinators.nondep_then LowParse.Spec.Combinators.and_then_kind LowParse.Spec.Combinators.parse_filter_kind ASN1.Spec.Value.OID.parse_asn1_oid_TLV_kind ASN1.Spec.TLV.parse_asn1_TLV_kind_of_type ASN1.Base.BOOLEAN FStar.Pervasives.Native.tuple2 ASN1.Spec.Value.OID.the_asn1_oid ASN1.Spec.Value.OID.parse_asn1_oid_TLV_of ASN1.Spec.TLV.parse_asn1_TLV_of_type ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.OCTET_STRING ASN1.Spec.Value.Envelop.inbound_envelop_tag_with_value_of ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV X509.BasicFields.Extension2.parse_x509_extension_payload_kind X509.BasicFields.Extension2.x509_extension_payload_t FStar.Ghost.hide
let parse_x509_extension_payload #k #t #p oid s =
  
((parse_asn1_oid_TLV_of oid) `nondep_then` (parse_asn1_TLV_of_type BOOLEAN))
`nondep_then`
(OCTET_STRING `parse_asn1_envelop_tag_with_TLV` s)