val long_packet_type:LP.enum long_packet_type_t (LPB.bitfield LPB.uint8 2)
let long_packet_type : LP.enum long_packet_type_t (LPB.bitfield LPB.uint8 2) = [
  Initial, 0uy;
  ZeroRTT, 1uy;
  Handshake, 2uy;
  Retry, 3uy;
]
val long_packet_type:LP.enum long_packet_type_t (LPB.bitfield LPB.uint8 2)
let long_packet_type:LP.enum long_packet_type_t (LPB.bitfield LPB.uint8 2) =
[Initial, 0uy; ZeroRTT, 1uy; Handshake, 2uy; Retry, 3uy]
QUIC.Spec.Header.Public.fst.checked
QUIC.Spec.VarInt.fsti.checked prims.fst.checked LowParse.Spec.Enum.fst.checked LowParse.Spec.BitSum.fst.checked LowParse.Spec.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
QUIC.Spec.Header.Public.fst
Prims.Cons FStar.Pervasives.Native.tuple2 QUIC.Spec.Header.Public.long_packet_type_t LowParse.BitFields.bitfield FStar.UInt8.t LowParse.BitFields.uint8 FStar.Pervasives.Native.Mktuple2 QUIC.Spec.Header.Public.Initial FStar.UInt8.__uint_to_t QUIC.Spec.Header.Public.ZeroRTT QUIC.Spec.Header.Public.Handshake QUIC.Spec.Header.Public.Retry Prims.Nil
module QUIC.Spec.Header.Public

module LP = LowParse.Spec
module LPB = LowParse.Spec.BitSum

inline_for_extraction
type header_form_t =
  | Long
  | Short

[@LPB.filter_bitsum'_t_attr]
inline_for_extraction
noextract
let header_form : LP.enum header_form_t (LPB.bitfield LPB.uint8 1) = [
  Long, 1uy;
  Short, 0uy;
]

[@LPB.filter_bitsum'_t_attr]
inline_for_extraction
noextract
let fixed_bit : LP.enum unit (LPB.bitfield LPB.uint8 1) = [
  (), 1uy;
]

inline_for_extraction
type long_packet_type_t =
  | Initial
  | ZeroRTT
  | Handshake
  | Retry

[@LPB.filter_bitsum'_t_attr]
inline_for_extraction
val long_packet_type:LP.enum long_packet_type_t (LPB.bitfield LPB.uint8 2)
LowParse.Spec.Enum.enum QUIC.Spec.Header.Public.long_packet_type_t
  (LowParse.BitFields.bitfield LowParse.BitFields.uint8 2)