Re: [Hol-info] About the use of symbol | in HOL4

[Jeremy Dawson]

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 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 
> 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 
> 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
>

--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] ?????? About the use of symbol | in HOL4

[Ada]

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] 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 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 
> 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 
> 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
>--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info