val constantByte_parser_kind : LowParse.Spec.Base.parser_kind
let constantByte_parser_kind =
  LP.strong_parser_kind 1 1 constantByte_parser_kind_metadata
module MiTLS.Format.Constants
open MiTLS

open FStar.Bytes

module LP = LowParse.SLow.Base
module U8 = FStar.UInt8

inline_for_extraction
let is_constantByte (c:byte) (x:byte): Tot bool = x = c

type constantByte (c:byte) = b:byte{is_constantByte c b}

inline_for_extraction
val constantByte_parser_kind_metadata: LP.parser_kind_metadata_t
/
prims.fst.checked LowParse.SLow.Base.fst.checked FStar.UInt8.fsti.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked
MiTLS.Format.Constants.fsti
LowParse.Spec.Base.parser_kind
LowParse.Spec.Base.strong_parser_kind MiTLS.Format.Constants.constantByte_parser_kind_metadata
let constantByte_parser_kind =
  
LP.strong_parser_kind 1 1 constantByte_parser_kind_metadata