Hey guys,
I am learning to use HOL4. I defined a function named "first" in HOL4. This
function can get the first n elements in a list. As follows:
- val first_def = Define`(first [] n = [] )
/\ (first (p::pl) 0 = [] )
/\ (first (p::pl) n = HD (p:
Hi Ada,
It's just
val fir_def = Define`(fir [] n = [] ) /\ (fir p 0 = [])`;
ie what's between the backquotes looks just like a statement in the HOL
logic
Cheers,
Jeremy
On 29/11/15 23:08, Ada wrote:> Thank you for your reply!
> if I want to use symbol | in defining a function in the HOL
Hi Ada,
In the first case you're trying to define a function in the HOL logic.
In the second case you're defining a SML function
Jeremy
On 29/11/15 22:15, Ada wrote:
> Hey guys,
>
> I am learning to use HOL. I find an interesting thing about the use of
> symbol | in HOL4.
> I defined an functi
Thank you for your reply!
if I want to use symbol | in defining a function in the HOL logic, how could I
use it ?
-- --
??: "Jeremy Dawson";;
: 2015??11??29??(??) 7:56
??: ""; "hol-info";
: Re: [Hol-info] Ab
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
