val tag_of_certificateExtension (x: certificateExtension) : extensionType
val tag_of_certificateExtension (x: certificateExtension) : extensionType
let tag_of_certificateExtension (x:certificateExtension) : extensionType = match x with
  | E_status_request _ -> Status_request
  | E_signed_certificate_timestamp _ -> Signed_certificate_timestamp
  | E_key_share _ -> Key_share
  | E_signature_algorithms_cert _ -> Signature_algorithms_cert
  | E_post_handshake_auth _ -> Post_handshake_auth
  | E_oid_filters _ -> Oid_filters
  | E_certificate_authorities _ -> Certificate_authorities
  | E_psk_key_exchange_modes _ -> Psk_key_exchange_modes
  | E_cookie _ -> Cookie
  | E_supported_versions _ -> Supported_versions
  | E_early_data _ -> Early_data
  | E_pre_shared_key _ -> Pre_shared_key
  | E_session_ticket _ -> Session_ticket
  | E_extended_master_secret _ -> Extended_master_secret
  | E_encrypt_then_mac _ -> Encrypt_then_mac
  | E_padding _ -> Padding
  | E_server_certificate_type _ -> Server_certificate_type
  | E_client_certificate_type _ -> Client_certificate_type
  | E_application_layer_protocol_negotiation _ -> Application_layer_protocol_negotiation
  | E_heartbeat _ -> Heartbeat
  | E_use_srtp _ -> Use_srtp
  | E_signature_algorithms _ -> Signature_algorithms
  | E_ec_point_formats _ -> Ec_point_formats
  | E_supported_groups _ -> Supported_groups
  | E_max_fragment_length _ -> Max_fragment_length
  | E_server_name _ -> Server_name
  | E_Unknown_extensionType v _ -> Unknown_extensionType v
module MiTLS.Parsers.CertificateExtension

(* This file has been automatically generated by EverParse. *)
open FStar.Bytes
module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module LP = LowParse.Spec.Base
module LS = LowParse.SLow.Base
module LSZ = LowParse.SLow.Base
module LPI = LowParse.Spec.AllIntegers
module LL = LowParse.Low.Base
module L = FStar.List.Tot
module B = LowStar.Buffer
module BY = FStar.Bytes
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST

open MiTLS.Parsers.ExtensionType
include MiTLS.Parsers.CertificateExtension_e_default
include MiTLS.Parsers.CertificateExtension_e_status_request
include MiTLS.Parsers.CertificateExtension_e_signed_certificate_timestamp

type certificateExtension =
  | E_status_request of certificateExtension_e_status_request
  | E_signed_certificate_timestamp of certificateExtension_e_signed_certificate_timestamp
  | E_key_share of certificateExtension_e_default
  | E_signature_algorithms_cert of certificateExtension_e_default
  | E_post_handshake_auth of certificateExtension_e_default
  | E_oid_filters of certificateExtension_e_default
  | E_certificate_authorities of certificateExtension_e_default
  | E_psk_key_exchange_modes of certificateExtension_e_default
  | E_cookie of certificateExtension_e_default
  | E_supported_versions of certificateExtension_e_default
  | E_early_data of certificateExtension_e_default
  | E_pre_shared_key of certificateExtension_e_default
  | E_session_ticket of certificateExtension_e_default
  | E_extended_master_secret of certificateExtension_e_default
  | E_encrypt_then_mac of certificateExtension_e_default
  | E_padding of certificateExtension_e_default
  | E_server_certificate_type of certificateExtension_e_default
  | E_client_certificate_type of certificateExtension_e_default
  | E_application_layer_protocol_negotiation of certificateExtension_e_default
  | E_heartbeat of certificateExtension_e_default
  | E_use_srtp of certificateExtension_e_default
  | E_signature_algorithms of certificateExtension_e_default
  | E_ec_point_formats of certificateExtension_e_default
  | E_supported_groups of certificateExtension_e_default
  | E_max_fragment_length of certificateExtension_e_default
  | E_server_name of certificateExtension_e_default
  | E_Unknown_extensionType: v:extensionType_repr{not (known_extensionType_repr v)} -> x:certificateExtension_e_default -> certificateExtension
/
prims.fst.checked MiTLS.Parsers.ExtensionType.fsti.checked MiTLS.Parsers.CertificateExtension_e_status_request.fsti.checked MiTLS.Parsers.CertificateExtension_e_signed_certificate_timestamp.fsti.checked MiTLS.Parsers.CertificateExtension_e_default.fsti.checked LowStar.Buffer.fst.checked LowParse.Spec.Base.fsti.checked LowParse.Spec.AllIntegers.fst.checked LowParse.SLow.Base.fst.checked LowParse.Low.Base.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked
MiTLS.Parsers.CertificateExtension.fsti
x: MiTLS.Parsers.CertificateExtension.certificateExtension
  -> MiTLS.Parsers.ExtensionType.extensionType
MiTLS.Parsers.CertificateExtension.certificateExtension MiTLS.Parsers.CertificateExtension_e_status_request.certificateExtension_e_status_request MiTLS.Parsers.ExtensionType.Status_request MiTLS.Parsers.CertificateExtension_e_signed_certificate_timestamp.certificateExtension_e_signed_certificate_timestamp MiTLS.Parsers.ExtensionType.Signed_certificate_timestamp MiTLS.Parsers.CertificateExtension_e_default.certificateExtension_e_default MiTLS.Parsers.ExtensionType.Key_share MiTLS.Parsers.ExtensionType.Signature_algorithms_cert MiTLS.Parsers.ExtensionType.Post_handshake_auth MiTLS.Parsers.ExtensionType.Oid_filters MiTLS.Parsers.ExtensionType.Certificate_authorities MiTLS.Parsers.ExtensionType.Psk_key_exchange_modes MiTLS.Parsers.ExtensionType.Cookie MiTLS.Parsers.ExtensionType.Supported_versions MiTLS.Parsers.ExtensionType.Early_data MiTLS.Parsers.ExtensionType.Pre_shared_key MiTLS.Parsers.ExtensionType.Session_ticket MiTLS.Parsers.ExtensionType.Extended_master_secret MiTLS.Parsers.ExtensionType.Encrypt_then_mac MiTLS.Parsers.ExtensionType.Padding MiTLS.Parsers.ExtensionType.Server_certificate_type MiTLS.Parsers.ExtensionType.Client_certificate_type MiTLS.Parsers.ExtensionType.Application_layer_protocol_negotiation MiTLS.Parsers.ExtensionType.Heartbeat MiTLS.Parsers.ExtensionType.Use_srtp MiTLS.Parsers.ExtensionType.Signature_algorithms MiTLS.Parsers.ExtensionType.Ec_point_formats MiTLS.Parsers.ExtensionType.Supported_groups MiTLS.Parsers.ExtensionType.Max_fragment_length MiTLS.Parsers.ExtensionType.Server_name MiTLS.Parsers.ExtensionType.extensionType_repr Prims.b2t Prims.op_Negation MiTLS.Parsers.ExtensionType.known_extensionType_repr MiTLS.Parsers.ExtensionType.Unknown_extensionType MiTLS.Parsers.ExtensionType.extensionType
let tag_of_certificateExtension (x: certificateExtension) : extensionType =
  
match x with
| E_status_request _ -> Status_request
| E_signed_certificate_timestamp _ -> Signed_certificate_timestamp
| E_key_share _ -> Key_share
| E_signature_algorithms_cert _ -> Signature_algorithms_cert
| E_post_handshake_auth _ -> Post_handshake_auth
| E_oid_filters _ -> Oid_filters
| E_certificate_authorities _ -> Certificate_authorities
| E_psk_key_exchange_modes _ -> Psk_key_exchange_modes
| E_cookie _ -> Cookie
| E_supported_versions _ -> Supported_versions
| E_early_data _ -> Early_data
| E_pre_shared_key _ -> Pre_shared_key
| E_session_ticket _ -> Session_ticket
| E_extended_master_secret _ -> Extended_master_secret
| E_encrypt_then_mac _ -> Encrypt_then_mac
| E_padding _ -> Padding
| E_server_certificate_type _ -> Server_certificate_type
| E_client_certificate_type _ -> Client_certificate_type
| E_application_layer_protocol_negotiation _ -> Application_layer_protocol_negotiation
| E_heartbeat _ -> Heartbeat
| E_use_srtp _ -> Use_srtp
| E_signature_algorithms _ -> Signature_algorithms
| E_ec_point_formats _ -> Ec_point_formats
| E_supported_groups _ -> Supported_groups
| E_max_fragment_length _ -> Max_fragment_length
| E_server_name _ -> Server_name
| E_Unknown_extensionType v _ -> Unknown_extensionType v