let t_limbs = U64
let t_limbs =
U64
Hacl.FFDHE.fst.checked
Spec.FFDHE.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Hacl.Impl.FFDHE.fst.checked Hacl.Bignum.Exponentiation.fsti.checked Hacl.Bignum.Definitions.fst.checked FStar.Pervasives.fsti.checked
Hacl.FFDHE.fst
Lib.IntTypes.U64
module Hacl.FFDHE

open Lib.IntTypes

module S = Spec.FFDHE
module DH = Hacl.Impl.FFDHE
module BD = Hacl.Bignum.Definitions
module BE = Hacl.Bignum.Exponentiation

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"
val t_limbs : Lib.IntTypes.inttype
Lib.IntTypes.inttype