val constantByte_serializer32 (c:byte)
  : Tot (LP.serializer32 #constantByte_parser_kind #(constantByte c) #(constantByte_parser c) (constantByte_serializer c))
val constantByte_serializer32 (c:byte)
  : Tot (LP.serializer32 #constantByte_parser_kind #(constantByte c) #(constantByte_parser c) (constantByte_serializer c))
let constantByte_serializer32 c
  = LP.serialize32_filter 
      #LP.parse_u8_kind #U8.t #LP.parse_u8 #LP.serialize_u8
      LP.serialize32_u8
      (is_constantByte c)
module MiTLS.Format.Constants
open MiTLS

open FStar.Bytes

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

let constantByte_parser_kind' = LP.parse_filter_kind LP.parse_u8_kind

let constantByte_parser_kind_metadata = constantByte_parser_kind'.LP.parser_kind_metadata

let constantByte_parser c =
  LP.parse_filter LP.parse_u8 (is_constantByte c)

let constantByte_parser32 c =
  LP.parse32_filter LP.parse32_u8 (is_constantByte c) (fun x -> is_constantByte c x)

let constantByte_serializer c
  = LP.serialize_filter 
      #LP.parse_u8_kind #U8.t #LP.parse_u8
      LP.serialize_u8 
      (is_constantByte c)
/
prims.fst.checked LowParse.SLow.fst.checked FStar.UInt8.fsti.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked
MiTLS.Format.Constants.fst
c: FStar.Bytes.byte
  -> LowParse.SLow.Base.serializer32 (MiTLS.Format.Constants.constantByte_serializer c)
FStar.Bytes.byte LowParse.SLow.Combinators.serialize32_filter LowParse.Spec.Int.parse_u8_kind FStar.UInt8.t LowParse.Spec.Int.parse_u8 LowParse.Spec.Int.serialize_u8 LowParse.SLow.Int.serialize32_u8 MiTLS.Format.Constants.is_constantByte LowParse.SLow.Base.serializer32 MiTLS.Format.Constants.constantByte_parser_kind MiTLS.Format.Constants.constantByte MiTLS.Format.Constants.constantByte_parser MiTLS.Format.Constants.constantByte_serializer
let constantByte_serializer32 c =
  
LP.serialize32_filter #LP.parse_u8_kind
  #U8.t
  #LP.parse_u8
  #LP.serialize_u8
  LP.serialize32_u8
  (is_constantByte c)