Re: [Hol-info] [HOL-INFO] programming mode in HOL4?

2015-11-14 Thread shengyu shen 
 --
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] [HOL-INFO] programming mode in HOL4?

2015-11-14 Thread shengyu shen 
 --
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] [HOL-INFO] programming mode in HOL4?

2015-11-14 Thread Ramana Kumar 
Use computeLib.EVAL.

On 14 November 2015 at 13:23, shengyu shen  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
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info