val validate_u8_with_error_code (c: error_code) : validator parse_u8
let validate_u8_with_error_code (c: error_code) : validator parse_u8 =
  validate_total_constant_size_with_error_code parse_u8 1uL c
val validate_u8_with_error_code (c: error_code) : validator parse_u8
let validate_u8_with_error_code (c: error_code) : validator parse_u8 =
validate_total_constant_size_with_error_code parse_u8 1uL c
LowParse.Low.Int.fsti.checked
prims.fst.checked LowParse.Spec.Int.fsti.checked LowParse.Low.Base.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked
LowParse.Low.Int.fsti
LowParse.Low.ErrorCode.error_code LowParse.Low.Base.validate_total_constant_size_with_error_code LowParse.Spec.Int.parse_u8_kind FStar.UInt8.t LowParse.Spec.Int.parse_u8 FStar.UInt64.__uint_to_t LowParse.Low.Base.validator
module LowParse.Low.Int
include LowParse.Spec.Int
include LowParse.Low.Base

inline_for_extraction
val read_u8: leaf_reader parse_u8

inline_for_extraction
val read_u16: leaf_reader parse_u16

inline_for_extraction
val read_u32: leaf_reader parse_u32

inline_for_extraction
val read_u64 : leaf_reader parse_u64

inline_for_extraction
val read_u64_le : leaf_reader parse_u64_le

inline_for_extraction
let validate_u8 () : validator parse_u8 =
  validate_total_constant_size parse_u8 1uL ()

inline_for_extraction
val validate_u8_with_error_code (c: error_code) : validator parse_u8
c: LowParse.Low.ErrorCode.error_code -> LowParse.Low.Base.validator LowParse.Spec.Int.parse_u8