mixing claim functions and compute functions in binary operators in the Resolute Prover

[reteprelief]

In the example below the user sees "Mixed claim and compute" as false with a single subresult "TrueClaim" as true. Both operands are evaluated for the AND result but only the claim function is shown. I suggest that if one operand is a claim function the other one should be too (exception is the "=>" operator where the left operand is required to be a compute function).

check_Mix (self:component) <=
** "Mixed claim and compute" **
check_False(self) and check_True_Claim(self) 

check_True_Claim (self:component) <=
** "TrueClaim" **
true

[reteprelief]

has been resolved by RC