Dear Jeremy,
I really appreciate your reply. However, the following sentence in my
question email is not my conclusion.
Here, a and c are independant, also b and c are independant.
However, a depends b.
It is the assumption. As I wrote in the goal,
(indep bern a c) /\ (indep bern b c)
Hi everyone，
Who know the different between with type and datatype in HOL4? I wanted to
define a new type for matrix in HOL4, but I might be confusing type with
datatype. I didn’t know how to start to define the type of matrix.
Who can help me ? Thank you very much. I’m looking for your
