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 mimic a state by passing it around explicitly. This is what the
WHILE
Hi Waqar,
First of all thanks for the reply. Your answer is very helpful to me.
What I want to achieve is to remove the first n items of the list each time and
operate on them,
and then continue to perform the same operation on the rest of the list until
the list is empty.
So after
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.
On 02/06/18 09:33, Ken Kubota wrote:
> Set theory (e.g., ZFC, the variant of Zermelo set theory in use today)
> takes a very different approach by giving the class status by default,
> and giving the set status only to those constructions often used.
> Compared with the type theoretic approach
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
