Hi Ada,
You have defined the function "first" on an arbitrary type list. It can be
specified for any type of list in the proof goal. For instance, you can
verify the following property on the "bool list":
g `!(L:bool list) n. n <= LENGTH L ==> (LENGTH (first L n) = n)`;
On Mon, Dec 7, 2015 at 7:18 PM, Ada <[email protected]> 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 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
>
>
--
Thanks and best regards,
Waqar Ahmed
Ph.D Candidate,
School of Electrical Engineering and Computer Science (SEECS),
National University of Science and Technology (NUST), H-12, Islamabad,
Pakistan
------------------------------------------------------------------------------
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
