Hi,guys
     I am working with HOL4.  
     I defined a function in HOL4,like following
     - fun ccdd a b c d  = if ((a = b) /\ (c = d)) then true else false;
     It responded that:
     ! Toplevel input:
    ! fun ccdd a b c d  = if ((a = b) /\ (c = d)) then true else false;
    !                         ^^^^^^^
    ! Type clash: expression of type
    !   bool
    ! cannot have type
    !   'a -> 'b
     I can't understand it.
     Who know the reason?
         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

Reply via email to