val string_of_namedGroup : _: MiTLS.Parsers.NamedGroup.namedGroup -> Prims.string
let string_of_namedGroup = function
  | Sect233k1 -> "sect233k1"
  | Sect233r1 -> "sect233r1"
  | Sect239k1 -> "sect239k1"
  | Sect283k1 -> "sect283k1"
  | Sect283r1 -> "sect283r1"
  | Sect409k1 -> "sect409k1"
  | Sect409r1 -> "sect409r1"
  | Sect571k1 -> "sect571k1"
  | Sect571r1 -> "sect571r1"
  | Secp224k1 -> "secp224k1"
  | Secp224r1 -> "secp224r1"
  | Secp256k1 -> "secp256k1"
  | Secp256r1 -> "secp256r1"
  | Secp384r1 -> "secp384r1"
  | Secp521r1 -> "secp521r1"
  | X25519 -> "x25519"
  | X448 -> "x448"
  | Ffdhe2048 -> "ffdhe2048"
  | Ffdhe3072 -> "ffdhe3072"
  | Ffdhe4096 -> "ffdhe4096"
  | Ffdhe6144 -> "ffdhe6144"
  | Ffdhe8192 -> "ffdhe8192"
  | Unknown_namedGroup _ -> "Unknown_namedGroup"
module MiTLS.Parsers.NamedGroup

(* 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


let namedGroup_repr = U16.t
inline_for_extraction let namedGroup_repr_eq (x1 x2: namedGroup_repr) : Tot bool = (x1 = x2)
let known_namedGroup_repr (v:U16.t) : bool = v `namedGroup_repr_eq` 6us || (v `namedGroup_repr_eq` 7us || (v `namedGroup_repr_eq` 8us || (v `namedGroup_repr_eq` 9us || (v `namedGroup_repr_eq` 10us || (v `namedGroup_repr_eq` 11us || (v `namedGroup_repr_eq` 12us || (v `namedGroup_repr_eq` 13us || (v `namedGroup_repr_eq` 14us || (v `namedGroup_repr_eq` 20us || (v `namedGroup_repr_eq` 21us || (v `namedGroup_repr_eq` 22us || (v `namedGroup_repr_eq` 23us || (v `namedGroup_repr_eq` 24us || (v `namedGroup_repr_eq` 25us || (v `namedGroup_repr_eq` 29us || (v `namedGroup_repr_eq` 30us || (v `namedGroup_repr_eq` 256us || (v `namedGroup_repr_eq` 257us || (v `namedGroup_repr_eq` 258us || (v `namedGroup_repr_eq` 259us || (v `namedGroup_repr_eq` 260us || (false))))))))))))))))))))))

type namedGroup =
  | Sect233k1
  | Sect233r1
  | Sect239k1
  | Sect283k1
  | Sect283r1
  | Sect409k1
  | Sect409r1
  | Sect571k1
  | Sect571r1
  | Secp224k1
  | Secp224r1
  | Secp256k1
  | Secp256r1
  | Secp384r1
  | Secp521r1
  | X25519
  | X448
  | Ffdhe2048
  | Ffdhe3072
  | Ffdhe4096
  | Ffdhe6144
  | Ffdhe8192
  | Unknown_namedGroup of (v:U16.t{not (known_namedGroup_repr v)})
/
prims.fst.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.NamedGroup.fsti
_: MiTLS.Parsers.NamedGroup.namedGroup -> Prims.string
MiTLS.Parsers.NamedGroup.namedGroup FStar.UInt16.t Prims.b2t Prims.op_Negation MiTLS.Parsers.NamedGroup.known_namedGroup_repr Prims.string
let string_of_namedGroup =
  
function
| Sect233k1 -> "sect233k1"
| Sect233r1 -> "sect233r1"
| Sect239k1 -> "sect239k1"
| Sect283k1 -> "sect283k1"
| Sect283r1 -> "sect283r1"
| Sect409k1 -> "sect409k1"
| Sect409r1 -> "sect409r1"
| Sect571k1 -> "sect571k1"
| Sect571r1 -> "sect571r1"
| Secp224k1 -> "secp224k1"
| Secp224r1 -> "secp224r1"
| Secp256k1 -> "secp256k1"
| Secp256r1 -> "secp256r1"
| Secp384r1 -> "secp384r1"
| Secp521r1 -> "secp521r1"
| X25519 -> "x25519"
| X448 -> "x448"
| Ffdhe2048 -> "ffdhe2048"
| Ffdhe3072 -> "ffdhe3072"
| Ffdhe4096 -> "ffdhe4096"
| Ffdhe6144 -> "ffdhe6144"
| Ffdhe8192 -> "ffdhe8192"
| Unknown_namedGroup _ -> "Unknown_namedGroup"