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 be violated by a function "rand". You can have underspecified functions though or model randomness / nondeterminism explicitly. Best Thomas Tuerk On 14/06/16 04:48, Ada wrote: > 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? > Thanks! > > > ------------------------------------------------------------------------------ > What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic > patterns at an interface-level. Reveals which users, apps, and protocols are > consuming the most bandwidth. Provides multi-vendor support for NetFlow, > J-Flow, sFlow and other flows. Make informed decisions using capacity > planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e > > > > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > ------------------------------------------------------------------------------ What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic patterns at an interface-level. Reveals which users, apps, and protocols are consuming the most bandwidth. Provides multi-vendor support for NetFlow, J-Flow, sFlow and other flows. Make informed decisions using capacity planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
