Operators accept Bools, [truth values](@ref nullary_operators), and [propositions](@ref propositions). However, boolean values cannot interoperate with truth values and propositions. Operations on boolean values is always eagerly evaluated, whereas operations on truth values and propositions is evaluated according to the operator's [Evaluation](@ref Interface.Evaluation) trait.
!!! info
Operations on propositions that have each been normalized eagerly evaluate to another normalized proposition.
This behavior is likely to be removed in v0.4.
Typing symbols with tab completion is performed by typing \, followed by the given characters, and then the [TAB] key. For example, ⊤ is typed with \top[TAB]. See also Tab Completion and Unicode Input.
Operator associativity determines how operators with the same precedence group their operands. For example, ∧ is left associative. Therefore, p ∧ q ∧ r is equivalent to (p ∧ q) ∧ r. Operator precedence determines how expressions with distinct operators are grouped together. Higher precedence operators will group their operands before lower precedence operators. For example, ∧ has a higher precedence than ∨. Therefore, p ∨ q ∧ r is equivalent to p ∨ (q ∧ r), even though both operators are left associative. See also Julia's documentation on Operator Precedence and Associativity.
!!! info
This associativity is determined by Julia's parser and is distinct from the Associativity trait used to specify the direction an operator folds.
!!! info
== has a precedence of 7, which is higher than that of several binary operators. For those cases, you may need to use parentheses. For example, p → q == r parses as p → (q == r) rather than (p → q) == r.
| Name | Symbol | Tab Completion | Associativity | Precedence |
|---|---|---|---|---|
tautology |
⊤ |
\top | none | 0 |
contradiction |
⊥ |
\bot | none | 0 |
identical |
𝒾 |
\scri | none | 0 |
not |
¬ |
\neg | right | 0 |
and |
∧ |
\wedge | left | 12 |
or |
∨ |
\vee | left | 11 |
imply |
→ |
\rightarrow | right | 4 |
exclusive_or |
↮ |
\nleftrightarrow | right | 4 |
converse_imply |
← |
\leftarrow | right | 4 |
not_and |
↑ |
\uparrow | right | 15 |
not_or |
↓ |
\downarrow | right | 15 |
not_imply |
↛ |
\nrightarrow | right | 4 |
not_exclusive_or |
↔ |
\leftrightarrow | right | 4 |
not_converse_imply |
↚ |
\nleftarrow | right | 4 |
conjunction |
⋀ |
\bigwedge | none | 0 |
disjunction |
⋁ |
\bigvee | none | 0 |
tautology
contradiction
identical
not
and
or
imply
exclusive_or
converse_imply
not_and
not_or
not_imply
not_exclusive_or
not_converse_imply
conjunction
disjunction
fold