Hey guys,
I am learning to use HOL. I find an interesting thing about the use of symbol |
in HOL4.
I defined an function named fir, as follows:
- val fir_def = Define`
(fir [] n = [] ) |
(fir p 0 = [])`;
But failed , it responsed that:
Don't expect to find a | in this position after a <beginning of input>
at line 5, character 22 and in compiler-generated text.
Exception raised at Absyn.Absyn:
in compiler-generated text:
Don't expect to find a | in this position after a <beginning of input>
at line 5, character 22 and in compiler-generated text.
! Uncaught exception:
! HOL_ERR
Then, I tried again , as follows:
- fun fir ([] , n) = []
| fir (p ,0 )= [] ;
It succeeded.
Now, I have two questions:
1??Why can't the symbol | be used in "Define"?
2??What are the differences between "Define" and "fun"?
Thanks! --Wish.------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
