Dear All,
I have a Query about Matrices. Can i write a definition in HOL light which
takes two matrices of dimensions real^N^M and real^Q^P and after a certain
operation output a vector with dimension real^(N*Q)^(M*P).
I was going through the theory and found finite_sum, which is the addition
of d
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;
!
