let lb (t:limb_t) =
  match t with
  | U32 -> buffer uint32
  | U64 -> buffer uint64
let lb (t: limb_t) =
match t with
| U32 -> buffer uint32
| U64 -> buffer uint64
Hacl.Bignum.MontArithmetic.fsti.checked
prims.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Bignum.MontArithmetic.fsti.checked Hacl.Bignum.Montgomery.fsti.checked Hacl.Bignum.Exponentiation.fsti.checked Hacl.Bignum.Definitions.fst.checked Hacl.Bignum.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Euclid.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Hacl.Bignum.MontArithmetic.fsti
Hacl.Bignum.Definitions.limb_t Lib.Buffer.buffer Lib.IntTypes.uint32 Lib.IntTypes.uint64
module Hacl.Bignum.MontArithmetic

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

open Hacl.Bignum.Definitions

module B = LowStar.Buffer
module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST

module Euclid = FStar.Math.Euclid
module S = Hacl.Spec.Bignum.MontArithmetic
module BE = Hacl.Bignum.Exponentiation
module BN = Hacl.Bignum
module BM = Hacl.Bignum.Montgomery

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

val _align_fsti : unit

inline_for_extraction noextract
val lb : t: Hacl.Bignum.Definitions.limb_t -> Type0
t: Hacl.Bignum.Definitions.limb_t -> Type0