ammer" and then rethink the issue.
Thank you for your reply！
Shang
-原始邮件-
发件人:"Chun Tian"
发送时间:2018-06-05 17:18:42 (星期二)
收件人: "尚亚龙" <2016210...@mail.buct.edu.cn>
抄送: "hol-info@lists.sourceforge.net"
主题: Re: [Hol-info] Loops in HOL4
Hi,
yo
> I learned a lot from it.
>
> I am not very familiar with the functions mentioned in your article.
>
> I will spend time to study them.
>
>
> Thank you again.
>
>
> Shang
> -原始邮件-
> 发件人:"Thomas Tuerk"
> 发送时间:2018-06-05 12:26:
: hol-info@lists.sourceforge.net
抄送:
主题: Re: [Hol-info] Loops in HOL4
Dear Shang,
reading your question, I was wondering, whether you really want to use a WHILE
loop. Usually you would rather use recursion in HOL. In higher order logic you
don't have a state that you can modify. Of course you can mim
t; *发送时间:*2018-06-05 07:43:50 (星期二)
> *收件人:* "尚亚龙" <2016210...@mail.buct.edu.cn>
> *抄送:* hol-info
> *主题:* Re: [Hol-info] Loops in HOL4
>
> I'm not sure what actually you desired with WHILE function but I
> can explain its functioning th
reading your reply, this problem can be solved.
thank you
Shang
-原始邮件-
发件人:"Waqar Ahmad" <12phdwah...@seecs.edu.pk>
发送时间:2018-06-05 07:43:50 (星期二)
收件人: "尚亚龙" <2016210...@mail.buct.edu.cn>
抄送: hol-info
主题: Re: [Hol-info] Loops in HOL4
I'm no
I'm not sure what actually you desired with WHILE function but I can
explain its functioning that might help you to define your function.
For instance, you can define a function that continue traversing over a
list until "P h" is true otherwise return the remaining part of the list.
!P L.
Hi everyone,
I'm just beginning to learn HOL4. And I have a question.
The problem is as follows: I have a list 'a',
I want to use a loop to retrieve the number of 'num' in a each time until the
list is empty,
and I see WHILE theorems can be used in the HOL library, but I can not
