val constantByte_parser (c: byte) : Tot (LP.parser constantByte_parser_kind (constantByte c))
val constantByte_parser (c: byte) : Tot (LP.parser constantByte_parser_kind (constantByte c))
let constantByte_parser c =
  LP.parse_filter LP.parse_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
/
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.Spec.Base.parser MiTLS.Format.Constants.constantByte_parser_kind
      (MiTLS.Format.Constants.constantByte c)
FStar.Bytes.byte LowParse.Spec.Combinators.parse_filter LowParse.Spec.Int.parse_u8_kind FStar.UInt8.t LowParse.Spec.Int.parse_u8 MiTLS.Format.Constants.is_constantByte LowParse.Spec.Base.parser MiTLS.Format.Constants.constantByte_parser_kind MiTLS.Format.Constants.constantByte
let constantByte_parser c =
  
LP.parse_filter LP.parse_u8 (is_constantByte c)