val u8_from_UInt8: (n:FStar.UInt8.t) -> u:uint8{uint_v #U8 u = UInt8.v n}
let u8_from_UInt8 x = x
val u8_from_UInt8: (n:FStar.UInt8.t) -> u:uint8{uint_v #U8 u = UInt8.v n}
let u8_from_UInt8 x =
x
Lib.RawIntTypes.fst.checked
prims.fst.checked Lib.IntTypes.fst.checked Lib.IntTypes.fst.checked FStar.Pervasives.fsti.checked
Lib.RawIntTypes.fst
FStar.UInt8.t Lib.IntTypes.uint8 Prims.b2t Prims.op_Equality Prims.int Prims.l_or Lib.IntTypes.range Lib.IntTypes.U8 FStar.UInt.size FStar.UInt8.n Lib.IntTypes.uint_v Lib.IntTypes.SEC FStar.UInt8.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
val u8_from_UInt8: (n:FStar.UInt8.t) -> u:uint8{uint_v #U8 u = UInt8.v n}
n: FStar.UInt8.t -> u2: Lib.IntTypes.uint8{Lib.IntTypes.uint_v u2 = FStar.UInt8.v n}