Hi Ada,
It still looks like you might be mixing up ML and HOL. Are you trying to
define an ML function, or a HOL function?
In ML, the conjunction of two Boolean expressions can be formed using the
"andalso" operator.
Now, maybe you already defined /\ like this, and gave it infix status:
infix /\;
fun op /\ (a, b) = a andalso b;
Then I would expect your definition to work.
But please note that this is a definition in ML. If you want to make a
definition in HOL, use Define.
For example:
val ccdd_def = Define`ccdd a b c d = if ((a = b) /\ (c = d)) then T else F`;
Cheers,
Ramana
On 30 June 2016 at 22:51, Ada <956066...@qq.com> wrote:
> 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
>
>
------------------------------------------------------------------------------
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
