val u8: n:nat{n < 0x100} -> uint8
let u8 n = u8 n
val u8: n:nat{n < 0x100} -> uint8
let u8 n =
u8 n
Hacl.Test.Ed25519.fst.checked
prims.fst.checked Lib.RawIntTypes.fsti.checked Lib.PrintBuffer.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Ed25519.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.Int32.fsti.checked FStar.HyperStack.All.fst.checked C.String.fsti.checked C.fst.checked
Hacl.Test.Ed25519.fst
Prims.nat Prims.b2t Prims.op_LessThan Lib.IntTypes.u8 Lib.IntTypes.uint8
module Hacl.Test.Ed25519

open FStar.HyperStack.All
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer
open Lib.PrintBuffer

module Ed25519 = Hacl.Ed25519

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

inline_for_extraction noextract
val u8: n:nat{n < 0x100} -> uint8
n: Prims.nat{n < 0x100} -> Lib.IntTypes.uint8