val bn_add1:
    #t:limb_t
  -> #aLen:size_pos
  -> a:lbignum t aLen
  -> b1:limb t ->
  carry t & lbignum t aLen
let bn_add1 #t #aLen a b1 =
  Hacl.Spec.Bignum.Addition.bn_add1 a b1
val bn_add1:
    #t:limb_t
  -> #aLen:size_pos
  -> a:lbignum t aLen
  -> b1:limb t ->
  carry t & lbignum t aLen
let bn_add1 #t #aLen a b1 =
Hacl.Spec.Bignum.Addition.bn_add1 a b1
Hacl.Spec.Bignum.fst.checked
prims.fst.checked Lib.LoopCombinators.fsti.checked Lib.ByteSequence.fsti.checked Hacl.Spec.Bignum.Squaring.fst.checked Hacl.Spec.Bignum.Multiplication.fst.checked Hacl.Spec.Bignum.Lib.fst.checked Hacl.Spec.Bignum.Karatsuba.fst.checked Hacl.Spec.Bignum.Convert.fst.checked Hacl.Spec.Bignum.Comparison.fst.checked Hacl.Spec.Bignum.Addition.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked
Hacl.Spec.Bignum.fst
Hacl.Spec.Bignum.Definitions.limb_t Lib.IntTypes.size_pos Hacl.Spec.Bignum.Definitions.lbignum Hacl.Spec.Bignum.Definitions.limb Hacl.Spec.Bignum.Addition.bn_add1 FStar.Pervasives.Native.tuple2 Hacl.Spec.Bignum.Base.carry
module Hacl.Spec.Bignum

module Loops = Lib.LoopCombinators


#reset-options "--z3rlimit 50 --fuel 0 --ifuel 0"
val bn_add1:
    #t:limb_t
  -> #aLen:size_pos
  -> a:lbignum t aLen
  -> b1:limb t ->
  carry t & lbignum t aLen
a: Hacl.Spec.Bignum.Definitions.lbignum t aLen -> b1: Hacl.Spec.Bignum.Definitions.limb t
  -> Hacl.Spec.Bignum.Base.carry t * Hacl.Spec.Bignum.Definitions.lbignum t aLen