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

Syntax

implies_expr ::= spec_expr ==>  spec_expr
explies_expr ::= spec_expr <==  spec_expr
iff_expr     ::= spec_expr <==> 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 the same syntactic precedence as ==> rather than the tighter precedence of ==, so it can often be used without extra parentheses in contexts where == would require them.