The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

OK,

For my needs I can do this:

I can create MS-DOS Batch file with first line like this:

echo %Time% > time.v

In file time.v I have this line (for example):

17:33:47,56

With some simply parsing I can change file time.v in something like:

Parameter seed : nat.
Hypothesis H_seed : seed=4756.

(I left just seconds and cents)

And now I can start Coq with:

coqtop.opt -batch -load-vernac-source time.v

Now I can generate list of pseudo-random numbers.

Sure, I have to be carefuly with some conditions of Random Number
Generation (prime numbers, big numbers enought and so on).

OK, you can say: It is a hypothesis or axiom and consistency is preserved:)

Greetings,

Marko Malikoviæ

> There is no time function and I hope there will never be one, because
> coq functions must be total and well defined, I want to be able to prove

-- 
dr. sc. Marko Malikoviæ
Filozofski fakultet u Rijeci