val x509_extensions_t_inbound : s: LowParse.Spec.Base.serializer p -> Type0
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
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
/
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 -> Type0
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.Base.serializer ASN1.Spec.Value.Envelop.inbound_envelop_tag_with_value_of X509.BasicFields.Extensions.x509_extensions_outmost_explicit_tag
let x509_extensions_t_inbound (#k: parser_kind) (#t: Type0) (#p: parser k t) (s: serializer p) =
  
inbound_envelop_tag_with_value_of x509_extensions_outmost_explicit_tag s