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 0 = [] )
/\ (first p n = HD p :: first (TL p) (n-1)) `;
Type of it was that > val it = ``:'a list -> num -> 'a list`` : hol_type
I tried some times to modify its type. if I want get the type of ``:bool list
-> num -> bool list`` : hol_type, how can I do that?
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=254741911&iu=/4140
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
