val create5 (x0 x1 x2 x3 x4: uint64) : list uint64
let create5 (x0 x1 x2 x3 x4:uint64) : list uint64 = [x0; x1; x2; x3; x4]
val create5 (x0 x1 x2 x3 x4: uint64) : list uint64
let create5 (x0 x1 x2 x3 x4: uint64) : list uint64 =
[x0; x1; x2; x3; x4]
Hacl.Spec.Ed25519.PrecompTable.fsti.checked
Spec.Ed25519.fst.checked Spec.Curve25519.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.Curve25519.Field51.Definition.fst.checked Hacl.Impl.Ed25519.Field51.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.List.Tot.fst.checked
Hacl.Spec.Ed25519.PrecompTable.fsti
Lib.IntTypes.uint64 Prims.Cons Prims.Nil Prims.list
module Hacl.Spec.Ed25519.PrecompTable

open FStar.Mul
open Lib.IntTypes
open Lib.Sequence

module F51 = Hacl.Impl.Ed25519.Field51
module SF51 = Hacl.Spec.Curve25519.Field51.Definition

module S = Spec.Ed25519
module SC = Spec.Curve25519
module FL = FStar.List.Tot

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"
val create5 (x0 x1 x2 x3 x4: uint64) : list uint64

    x0: Lib.IntTypes.uint64 ->
    x1: Lib.IntTypes.uint64 ->
    x2: Lib.IntTypes.uint64 ->
    x3: Lib.IntTypes.uint64 ->
    x4: Lib.IntTypes.uint64
  -> Prims.list Lib.IntTypes.uint64