val parse_x509_extensions_TLV (#k: parser_kind) (#t: Type0) (#p: parser k t) (s: serializer p)
    : parser (parse_asn1_envelop_tag_with_TLV_kind x509_extensions_outmost_explicit_tag)
      (x509_extensions_t_inbound s)
val parse_x509_extensions_TLV (#k: parser_kind) (#t: Type0) (#p: parser k t) (s: serializer p)
    : parser (parse_asn1_envelop_tag_with_TLV_kind x509_extensions_outmost_explicit_tag)
      (x509_extensions_t_inbound s)
let parse_x509_extensions_TLV
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (s: serializer p)
: parser (parse_asn1_envelop_tag_with_TLV_kind x509_extensions_outmost_explicit_tag) (x509_extensions_t_inbound s)
= x509_extensions_t_inbound s
  `coerce_parser`
  parse_asn1_envelop_tag_with_TLV
  (* tag *) x509_extensions_outmost_explicit_tag
  (*  s  *) s
module X509.BasicFields.Extensions

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

let x509_extensions_outmost_explicit_tag: asn1_tag_t
= CUSTOM_TAG CONTEXT_SPECIFIC CONSTRUCTED 3uy

inline_for_extraction
let x509_extensions_t_inbound
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (s: serializer p)
= inbound_envelop_tag_with_value_of
  (* tag *) x509_extensions_outmost_explicit_tag
  (*  s  *) s
/
X509.Base.fst.checked prims.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.Base.fsti.checked FStar.UInt8.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.Extensions.fsti
s: LowParse.Spec.Base.serializer p
  -> LowParse.Spec.Base.parser (ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind X509.BasicFields.Extensions.x509_extensions_outmost_explicit_tag
        )
      (X509.BasicFields.Extensions.x509_extensions_t_inbound s)
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.Base.serializer LowParse.Spec.Base.coerce_parser X509.BasicFields.Extensions.x509_extensions_t_inbound ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind X509.BasicFields.Extensions.x509_extensions_outmost_explicit_tag ASN1.Spec.Value.Envelop.inbound_envelop_tag_with_value_of ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV
let parse_x509_extensions_TLV (#k: parser_kind) (#t: Type0) (#p: parser k t) (s: serializer p)
    : parser (parse_asn1_envelop_tag_with_TLV_kind x509_extensions_outmost_explicit_tag)
      (x509_extensions_t_inbound s) =
  
(x509_extensions_t_inbound s)
`coerce_parser`
(parse_asn1_envelop_tag_with_TLV x509_extensions_outmost_explicit_tag s)