val x509_extension_t' : oid: ASN1.Base.datatype_of_asn1_type ASN1.Base.OID -> s: LowParse.Spec.Base.serializer p -> Type0
let x509_extension_t'
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (oid: datatype_of_asn1_type OID)
  (s: serializer p)
= parse_filter_refine (filter_asn1_oid_TLV_of oid)
  `tuple2`
  datatype_of_asn1_type BOOLEAN
  `tuple2`
 (OCTET_STRING `inbound_envelop_tag_with_value_of` s)
module X509.BasicFields.Extension

open ASN1.Spec

open X509.Base

// inline_for_extraction
// type x509_extension_t
//   (#k: parser_kind)
//   (#t: Type0)
//   (#p: parser k t)
//   (oid: datatype_of_asn1_type OID)
//   (s: serializer p)
// = { x509_extID      : x:datatype_of_asn1_type OID {x == oid};
//     x509_extCritical: datatype_of_asn1_type BOOLEAN;
//     x509_extValue   : OCTET_STRING `inbound_envelop_tag_with_value_of` s }

(* one extension *)
/
X509.Base.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked
X509.BasicFields.Extension.fsti
oid: ASN1.Base.datatype_of_asn1_type ASN1.Base.OID -> s: LowParse.Spec.Base.serializer p -> Type0
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser ASN1.Base.datatype_of_asn1_type ASN1.Base.OID LowParse.Spec.Base.serializer FStar.Pervasives.Native.tuple2 LowParse.Spec.Combinators.parse_filter_refine ASN1.Spec.Value.OID.filter_asn1_oid_TLV_of ASN1.Base.BOOLEAN ASN1.Spec.Value.Envelop.inbound_envelop_tag_with_value_of ASN1.Base.OCTET_STRING
let x509_extension_t'
      (#k: parser_kind)
      (#t: Type0)
      (#p: parser k t)
      (oid: datatype_of_asn1_type OID)
      (s: serializer p)
     =
  
((parse_filter_refine (filter_asn1_oid_TLV_of oid)) `tuple2` (datatype_of_asn1_type BOOLEAN))
`tuple2`
(OCTET_STRING `inbound_envelop_tag_with_value_of` s)