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
