major cleanup of tsig datastructures and extend/merge operations; fixes old bugs in classes/arities code; proper treatment of nonterminals and syntax-only types;
Exor = Main +
constdefs
exor :: bool => bool => bool
"exor A B == (A & ~B) | (~A & B)"
end