Adding a new boolean data type for labels. Need to clearly distinguish between object variables and meta variables. Unification is required for meta-variables (as in existing version for angles) but is forbidden for object variables. In terms of operations, the most important are XOR and negation, but the all the usual connectives could be useful, with algebraic simplifications performed automatically.
Would also be good to hook into some kind of satisfiability checker to decide if expressions are equivalent or uniformly true/false. (This last step was essential in the proof of the correctness of the Steane Code.)
A partial implementation of this works (XOR and negation) be considering Bool as the field F2, and uses \top and \bot symbols. I would need to discuss the other parts with you to know if I could implement them.
Adding a new boolean data type for labels. Need to clearly distinguish between object variables and meta variables. Unification is required for meta-variables (as in existing version for angles) but is forbidden for object variables. In terms of operations, the most important are XOR and negation, but the all the usual connectives could be useful, with algebraic simplifications performed automatically.
Would also be good to hook into some kind of satisfiability checker to decide if expressions are equivalent or uniformly true/false. (This last step was essential in the proof of the correctness of the Steane Code.)