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

[Hol-info] some questions about the use of HD and TL in listTheory

[Ada]

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::pl) :: first (TL (p::pl)) 
(n-1)) `;
<>
Equations stored under "first_def".
Induction stored under "first_ind".
> val first_def =
|- (!n. first [] n = []) /\ (!pl p. first (p::pl) 0 = []) /\
   !v4 pl p.
 first (p::pl) (SUC v4) =
 HD (p::pl)::first (TL (p::pl)) (SUC v4 - 1) : thm
 In which, I saw HD and TL had been defined in listTheory. HD gets the first 
element in a list, TL gets the last.
  
 But , when I tried to use "first", failed. As followes:
  
 - first ([0,1,0,1,0],3);
! Toplevel input:
! first ([0,1,0,1,0],3);
! ^
! Type clash: expression of type
!   ('a -> bool) -> 'a list -> 'a
! cannot have type
!   'b * 'c -> 'a list -> 'a
 
- first  [0,1,0,1,0] 3;
! Toplevel input:
! first  [0,1,0,1,0] 3;
! ^^
! Type clash: expression of type
!   'a list
! cannot have type
!   'b -> bool
  
 I was wondering why it failed. Could anyone find the reasion?
  
 Thanks! --Wish.--
Go from Idea to Many App Stores Faster with Intel(R) XDK
Give your users amazing mobile app experiences with Intel(R) XDK.
Use one codebase in this all-in-one HTML5 development environment.
Design, debug & build mobile apps & 2D/3D high-impact games for multiple OSs.
http://pubads.g.doubleclick.net/gampad/clk?id=254741551=/4140___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info