# Prooftoys syntax quick reference

For more complete and precise information, see the full reference.

## Logic operators

Concept | English | Symbol | Text entry |
---|---|---|---|

Untrue | not | `not` |
not |

At least one true | or | `|` |
| |

Both true | and | `&` |
& |

Conditional | implies | `=>` |
=> |

Equivalent | `==` |
== | |

True for all | for all | `forall` |
forall |

True for some | exists | `exists` |
exists |

Precedence of infix operators in order from highest to lowest,
is `&, |, =>, ==`

.

The rest are functions, which bind tighter than
infix operators, so `not a & b`

means the same as `(not a) & b`

.

## Basic math

Basic binary math operations are: `+, -, *, /,
**` (exponentiation). Exponentiation has the highest precedence,
followed by multiplication and division, followed by addition and
subtraction. The negative of a number is expressed by the function
`neg`

, which displays as a prefix `-`

.

## Variables and constants

Variable names have a single alphabetic character, such as `x`

or `A`

.
The single letter may be followed by digits or a single underscore and
then digits. A variable name may also begin with `$`

, but these are
mainly intended to be introduced by the system.

Names with multiple alphabetic characters are always constants, and may also include digits.

The characters `".", “,”, “(”, “{”, “["` are reserved as parts
of the syntax. Sequences of characters that are not letters or digits
and not reserved for the syntax are also constants.