Implication (==>, <==, and <==>) #

Syntax #

V@[implies_expr] ::= V@[spec_expr] ==>  V@[spec_expr]
V@[explies_expr] ::= V@[spec_expr] <==  V@[spec_expr]
V@[iff_expr]     ::= V@[spec_expr] <==> V@[spec_expr]

Typing #

All three operators require both sides to have type bool and return bool.

Semantics #

P ==> Q, read P implies Q, is true whenever P is false or Q is true:

P ==> Q  ≡  !P || Q

P <== Q (P is implied by Q) is the converse: it is equivalent to Q ==> P. It is sometimes useful for readability when the consequent is more naturally written first.

P <==> Q (P if and only if Q) is true when both sides have the same truth value:

P <==> Q  ≡  P == Q

Note that <==> has lower syntactic precedence than ==> and <==, and much lower precedence than ==, so it can often be used without extra parentheses in contexts where == would require them.