|
From: A. <956...@qq...> - 2016-06-30 12:51:40
|
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! |