FST is a function in logic, not in ML.
In this case, there does happen to be a similar function, called fst, in ML.
Are you trying to specify/prove something in logic? Or are you trying to
write an ML program?
On 22 June 2016 at 18:21, Ada <956066...@qq.com> wrote:
> Hi,guys
> I am working with HOL4.
> FST is in pairTheory, its definition is
>
> [*FST*] Theorem
>
> |- ∀x y. FST (x,y) = x
>
> But, When I use it like following:
>
> val n = FST (1,2);
>
> It responses:
>
> ! Toplevel input:
> ! val n = FST (1,2);
> ! ^^^
> ! Type clash: expression of type
> ! thm
> ! cannot have type
> ! 'a -> 'b
>
> What is the reason? Does anyone know how to use it?
>
> Thanks!
>
>
> ------------------------------------------------------------------------------
> Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
> Francisco, CA to explore cutting-edge tech and listen to tech luminaries
> present their vision of the future. This family event has something for
> everyone, including kids. Get more information and register today.
> http://sdm.link/attshape
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
