val parse_constint32le_kind:parser_kind
let parse_constint32le_kind
: parser_kind
= strong_parser_kind 4 4 None
val parse_constint32le_kind:parser_kind
let parse_constint32le_kind:parser_kind =
strong_parser_kind 4 4 None
LowParse.Spec.ConstInt32.fst.checked
prims.fst.checked LowParse.Spec.Int32le.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.Base.fsti.checked LowParse.Math.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Endianness.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.ConstInt32.fst
LowParse.Spec.Base.strong_parser_kind FStar.Pervasives.Native.None LowParse.Spec.Base.parser_kind_metadata_some
module LowParse.Spec.ConstInt32

(* LowParse specification module for parsing 32 bits = 4 bytes unsigned constants

   Examples:

   uint32 foo = 5
   uint32_le foo = 7

*)

(* TODO: support big endian constants *)

include FStar.Endianness

include LowParse.Spec.Base
include LowParse.Spec.Combinators
include LowParse.Spec.Int32le

module U32 = FStar.UInt32
module U8 = FStar.UInt8
module Seq = FStar.Seq
module M = LowParse.Math

let constint32
  (v: nat { 0 <= v /\ v < 4294967296 } )
: Tot Type
= (u: U32.t { U32.v u == v } )

inline_for_extraction
let parse_constint32le_kind
val parse_constint32le_kind:parser_kind
LowParse.Spec.Base.parser_kind