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
