val be_to_n_0 (#t: Type) (#tot: nat) (u: uinttype t tot) : Tot (be_to_n_t u 0)
let be_to_n_0
  (#t: Type)
  (#tot: nat)
  (u: uinttype t tot)
: Tot (be_to_n_t u 0)
= fun x ->
  E.reveal_be_to_n (B.reveal x);
  u.zero
val be_to_n_0 (#t: Type) (#tot: nat) (u: uinttype t tot) : Tot (be_to_n_t u 0)
let be_to_n_0 (#t: Type) (#tot: nat) (u: uinttype t tot) : Tot (be_to_n_t u 0) =
fun x ->
  E.reveal_be_to_n (B.reveal x);
  u.zero
LowParse.SLow.Endianness.fst.checked
prims.fst.checked LowParse.Spec.Endianness.fst.checked LowParse.Endianness.fsti.checked LowParse.Bytes32.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked
LowParse.SLow.Endianness.fst
Prims.nat LowParse.Spec.Endianness.uinttype FStar.Bytes.lbytes LowParse.Spec.Endianness.__proj__UIntType__item__zero Prims.unit FStar.Endianness.reveal_be_to_n FStar.Bytes.reveal Prims.eq2 LowParse.Spec.Endianness.__proj__UIntType__item__v FStar.Endianness.be_to_n LowParse.SLow.Endianness.be_to_n_t
module LowParse.SLow.Endianness
include LowParse.Spec.Endianness

module U8 = FStar.UInt8
module E = LowParse.Endianness
module B = LowParse.Bytes32
module U32 = FStar.UInt32

open FStar.Mul

inline_for_extraction
noextract
let be_to_n_t
  (#t: Type)
  (#tot: nat)
  (u: uinttype t tot)
  (len: nat { len <= tot })
: Tot Type
= (x: B.lbytes len) ->
  Tot (y: t { u.v y == E.be_to_n (B.reveal x) })

inline_for_extraction
noextract
let be_to_n_0
  (#t: Type)
  (#tot: nat)
  (u: uinttype t tot)
val be_to_n_0 (#t: Type) (#tot: nat) (u: uinttype t tot) : Tot (be_to_n_t u 0)
u9: LowParse.Spec.Endianness.uinttype t tot -> LowParse.SLow.Endianness.be_to_n_t u9 0