val bn_add_eq_len: #t:limb_t -> len:size_t -> bn_add_eq_len_st t len
let bn_add_eq_len #t aLen a b res =
  Hacl.Bignum.Addition.bn_add_eq_len aLen a b res
val bn_add_eq_len: #t:limb_t -> len:size_t -> bn_add_eq_len_st t len
let bn_add_eq_len #t aLen a b res =
Hacl.Bignum.Addition.bn_add_eq_len aLen a b res
Hacl.Bignum.fst.checked
prims.fst.checked LowStar.Ignore.fsti.checked Lib.ByteBuffer.fsti.checked Hacl.Spec.Bignum.fst.checked Hacl.Bignum.Multiplication.fst.checked Hacl.Bignum.Lib.fst.checked Hacl.Bignum.Karatsuba.fst.checked Hacl.Bignum.Convert.fst.checked Hacl.Bignum.Comparison.fst.checked Hacl.Bignum.Addition.fst.checked FStar.UInt32.fsti.checked FStar.ST.fst.checked FStar.Pervasives.fsti.checked
Hacl.Bignum.fst
Hacl.Bignum.Definitions.limb_t Lib.IntTypes.size_t Hacl.Bignum.Definitions.lbignum Hacl.Bignum.Addition.bn_add_eq_len Hacl.Spec.Bignum.Base.carry
module Hacl.Bignum

friend Hacl.Spec.Bignum

#reset-options "--z3rlimit 50 --fuel 0 --ifuel 0"

let bn_add1 #t aLen a b1 res =
  Hacl.Bignum.Addition.bn_add1 aLen a b1 res

let bn_sub1 #t aLen a b1 res =
  Hacl.Bignum.Addition.bn_sub1 aLen a b1 res
val bn_add_eq_len: #t:limb_t -> len:size_t -> bn_add_eq_len_st t len
len: Lib.IntTypes.size_t -> Hacl.Bignum.bn_add_eq_len_st t len