Incompatible
Declaring that two rules should not both be enabled
Example:
(theory-invariant (incompatible (:rewrite left-to-right)
(:rewrite right-to-left)))
General Form:
(incompatible rune1 rune2)
where rune1 and rune2 are two specific runes. The
arguments are not evaluated. Invariant is just a macro that expands into
a term that checks that not both runes are enabled. See theory-invariant. Also see incompatible! for a variant that insists
the arguments are indeed runes, not merely having the shapes of runes.
