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 /\
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;
!
