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 succeed,
So I would like to ask how to implement the WHILE theorem,
if you can, please attach an example to explain. Thank you!
Shang
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
