ction in the HOL logic, how
> could I use it ?
>
>
> -- --
> *??:* "Jeremy Dawson";;
> *:* 2015??11??29??(??) 7:56
> *??????:* "????";
> "hol-info";
> *:* Re: [Hol-info
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
quot;;
????: Re: [Hol-info] About the use of symbol | in HOL4
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
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
