val le_to_n : b:bytes -> Tot nat (decreases (S.length b))
let rec le_to_n b =
  if S.length b = 0 then 0
  else U8.v (S.head b) + pow2 8 * le_to_n (S.tail b)
val le_to_n : b:bytes -> Tot nat (decreases (S.length b))
let rec le_to_n b =
if S.length b = 0 then 0 else U8.v (S.head b) + pow2 8 * le_to_n (S.tail b)
FStar.Krml.Endianness.fst.checked
prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.All.fst.checked FStar.Classical.fsti.checked
FStar.Krml.Endianness.fst
FStar.Krml.Endianness.bytes Prims.op_Equality Prims.int FStar.Seq.Base.length FStar.UInt8.t Prims.bool Prims.op_Addition FStar.UInt8.v FStar.Seq.Properties.head FStar.Mul.op_Star Prims.pow2 FStar.Krml.Endianness.le_to_n FStar.Seq.Properties.tail Prims.nat
module FStar.Krml.Endianness

open FStar.Mul
open FStar.HyperStack.All

module U8 = FStar.UInt8
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module Math = FStar.Math.Lemmas
module S = FStar.Seq

(* Selectively imported from Hacl*'s FStar.Endianness.fst library, with several
name changes *)

inline_for_extraction noextract
type bytes = S.seq U8.t

/// lt_to_n interprets a byte sequence as a little-endian natural number
[@(deprecated "FStar.Endianness.le_to_n")]
val le_to_n : b:bytes -> Tot nat (decreases (S.length b))
val le_to_n : b:bytes -> Tot nat (decreases (S.length b))
b: FStar.Krml.Endianness.bytes -> Prims.Tot Prims.nat