Use computeLib.EVAL. On 14 November 2015 at 13:23, shengyu shen <[email protected]> wrote:
> Dear all: > > I have some experience in ACL2 and COQ, which have a programming mode, in > which I can try running some function. For example, I define a fact > function that compute the factorial of a particular integer n. And in both > ACL2 and Coq, I can run this function to test if it is defined corectly. > > But in HOL4, how can I do this? > > Shen > > > ------------------------------------------------------------------------------ > > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info > >
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
