val bn_from_uint: #t:limb_t -> len:size_pos -> x:limb t -> lbignum t len
let bn_from_uint #t len x =
  let b = create len (uint #t 0) in
  b.[0] <- x
val bn_from_uint: #t:limb_t -> len:size_pos -> x:limb t -> lbignum t len
let bn_from_uint #t len x =
let b = create len (uint #t 0) in
b.[ 0 ] <- x
Hacl.Spec.Bignum.Convert.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Hacl.Spec.Bignum.Convert.fst
Hacl.Spec.Bignum.Definitions.limb_t Lib.IntTypes.size_pos Hacl.Spec.Bignum.Definitions.limb Lib.Sequence.op_String_Assignment Lib.Sequence.lseq Prims.l_and Prims.eq2 FStar.Seq.Base.seq Lib.Sequence.to_seq FStar.Seq.Base.create Lib.IntTypes.mk_int Lib.IntTypes.SEC Prims.l_Forall Prims.nat Prims.l_imp Prims.b2t Prims.op_LessThan Lib.Sequence.index Lib.Sequence.create Lib.IntTypes.uint Hacl.Spec.Bignum.Definitions.lbignum
module Hacl.Spec.Bignum.Convert

open FStar.Mul

open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence

open Hacl.Spec.Bignum.Definitions


#reset-options "--z3rlimit 50 --fuel 0 --ifuel 0"
val bn_from_uint: #t:limb_t -> len:size_pos -> x:limb t -> lbignum t len
len: Lib.IntTypes.size_pos -> x: Hacl.Spec.Bignum.Definitions.limb t
  -> Hacl.Spec.Bignum.Definitions.lbignum t len