val u128_to_UInt128: (u:uint128) -> n:UInt128.t{uint_v #U128 u = UInt128.v n}
let u128_to_UInt128 x = x
val u128_to_UInt128: (u:uint128) -> n:UInt128.t{uint_v #U128 u = UInt128.v n}
let u128_to_UInt128 x =
x
Lib.RawIntTypes.fst.checked
prims.fst.checked Lib.IntTypes.fst.checked Lib.IntTypes.fst.checked FStar.Pervasives.fsti.checked
Lib.RawIntTypes.fst
Lib.IntTypes.uint128 FStar.UInt128.t Prims.b2t Prims.op_Equality Prims.int Prims.l_or Lib.IntTypes.range Lib.IntTypes.U128 FStar.UInt.size FStar.UInt128.n Lib.IntTypes.uint_v Lib.IntTypes.SEC FStar.UInt128.v
module Lib.RawIntTypes

open Lib.IntTypes

(* This module offers direct access to the internals of IntTypes.
   Typechecking it requires full access to IntTypes.fst (not just IntTypes.fsti)
   Use only if you need to, because using this module will load more F* dependencies.
   More importantly, using the u*_to_UInt* functions BREAKS secret independence.  *)

friend Lib.IntTypes

let u8_from_UInt8 x = x

let u16_from_UInt16 x = x

let u32_from_UInt32 x = x

let u64_from_UInt64 x = x

let u128_from_UInt128 x = x

let size_from_UInt32 x = x

let u8_to_UInt8 x = x

let u16_to_UInt16 x = x

let u32_to_UInt32 x = x

let u64_to_UInt64 x = x
val u128_to_UInt128: (u:uint128) -> n:UInt128.t{uint_v #U128 u = UInt128.v n}
u11: Lib.IntTypes.uint128 -> n: FStar.UInt128.t{Lib.IntTypes.uint_v u11 = FStar.UInt128.v n}