HOL syntax for lists uses semicolons (;) to separate list elements, not
commas (,).
On 30 November 2015 at 18:42, Ada <ada.k...@qq.com> 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=254741551&iu=/4140
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
