Hi Ada,
when you enter
first ([0,1,0,1,0],3);
this refers to the SML function first whose type is given by
first ;
val it = fn: ('a -> bool) -> 'a list -> 'a
What you want is the HOL term
``first ([0,1,0,1,0],3)``
which will also give you a type error, since your definition of first
requires it to be used as follows
``first [(0,1,0,1,0)] 3``
To help you see what's happening,
show_types := true ;
val it = (): unit
> ``first`` ;
<<HOL message: inventing new type variable names: 'a>>
val it =
``(first :α list -> num -> α list)``:
Suggest you get familiar with types in SML before spending too much time
on HOL
Cheers,
Jeremy
On 30/11/15 18:42, Ada wrote:
> 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)) `;
> <<HOL message: inventing new type variable names: 'a>>
> 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&iu=/4140
>
>
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
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=254741911&iu=/4140
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
