Hi Ada,
could you explain in more detail what you want? I did not get wether you
need in ML or in the logic. Moreover, I did not get the "x = ..." part.
In ML, look at the structure "Random".
In the logic such a function cannot exists, since forall f, args "f args
= f args" holds, which would
Hi,guys
I am working with HOL4. Now, I need a function that can produce random
number.
For example, supposing that function rand can create a random number, then
x=rand ()/LENGTH, where x is a number between 1 and LENGTH.
Does anyone know this?