Arrow variants: => and <=> vs → and ↔, which means what
-> and → are implication; <-> and ↔ are the biconditional. The fat arrows => and <=> are rejected, because they mean implication in some tools, a function in JavaScript, and a rewrite step in others.
The two diagnostics are recorded below: => is not a supported operator, use -> for implication; <=> is not a supported operator, use <-> for a biconditional. The repairs are one character each. The engine prints the thin arrows in the words and programming notations and the Unicode arrows → and ↔ in the mathematical and algebra notations, and accepts both on input.
The fat arrow's meanings elsewhere are the reason: in JavaScript and C# => introduces a function; in some proof assistants and in SMT-LIB it is implication; in rewriting it marks a step; in Perl and PHP it separates keys and values. <=> is a comparison operator in Perl, Ruby and C++. Reading either as a logical connective would be right for some sources and silently wrong for others.
Beyond spelling, remember what the arrows mean. A -> B is FALSE only when A is TRUE and B is FALSE, and chains associate to the right. A <-> B is TRUE when A and B agree, and a chain of <-> is rejected until bracketed. The implication and biconditional pages have the tables, and the comparison page sets the two side by side.
What the parser says
| You typed | Code | Why it is rejected | Repair offered |
|---|---|---|---|
| A => B | unsupported-operator | `=>` is not a supported operator. Use `->` for implication. | Replace with -> |
| A <=> B | unsupported-operator | `<=>` is not a supported operator. Use `<->` for a biconditional. | Replace with <-> |
The common slip
Pasting A => B from SMT-LIB or a proof script and getting a rejection. The intent is clear and the repair is ->; the refusal exists so that x => x + 1 from JavaScript is not read as an implication.
Questions
Does ⇒ (the double arrow symbol) work?
No, only -> and → for implication and <-> and ↔ for the biconditional. Double-shafted Unicode arrows are not accepted, for the same reason as =>.
Is -> the same as → in the engine?
Yes: they are two spellings of one operator. Which is printed depends on the notation you select.
Related
Tools
- Logical equivalence checker: two expressions, exact verdict, counterexample
- Truth table generator: any Boolean expression, up to 12 variables, with intermediate columns
See also
- Implication (→, if–then): truth table and why a false antecedent makes it true
- Biconditional (↔, if and only if): truth table and examples
- Logic symbols: meanings, LaTeX, Unicode and how to type them
- Boolean logic in SMT-LIB: declare-const, assert and check-sat with Z3
- Boolean logic in JavaScript: &&, ||, !, truthiness and precedence
- Implication vs biconditional
Pitfalls
Generated from the Tangibool engine, semantics tangibool-semantics/1, engine 1.0.0, build . Every table, map, simplification and verdict on these pages was computed by the Tangibool engine when the site was built, and every claim was re-checked by the same exact checker the app uses. Limits are stated where they apply. © 2026 Foreranger LTD.