You can access to a quick pdf summary about the tla+ language here: https://lamport.azurewebsites.net/tla/summary-standalone.pdf.

This is a web accessible version.

module M

Begins the module or submodule named M.

extends M1, ..., Mn

Incorporates the declarations, definitions, assumptions, and theorems from the modules named M1, ..., Mn into the current module.

constants C1, ..., Cn

Declares the Cj to be constant parameters (rigid variables). Each Cj is either an identifier or has the form C( , ..., ), the latter form indicating that C is an operator with the indicated number of arguments.

variables x1, ..., xn

Declares the xj to be variables (parameters that are flexible variables).

assume P

Asserts P as an assumption.

F(x1, ..., xn) Δ = exp

Defines F to be the operator such that F(e1, ..., en) equals exp with each identifier xk replaced by ek. (For n = 0, it is written F Δ = exp.)

f[x ∈ S] Δ = exp

Defines f to be the function with domain S such that f[x] = exp for all x in S. (The symbol f may occur in exp, allowing a recursive definition.)

instance M with p1 ← e1, ..., pm ← em

For each defined operator F of module M, this defines F to be the operator whose definition is obtained from the definition of F in M by replacing each declared constant or variable pj of M with ej. (If m = 0, the "with" is omitted.)

theorem P

Asserts that P can be proved from the definitions and assumptions of the current module.

local def

Makes the definition(s) of def (which may be a definition or an instance statement) local to the current module, thereby not obtained when extending or instantiating the module.

if p then e1 else e2 [e1 if p is true, else e2]

case p1 → e1 ... pn → en

case p1 → e1 ... pn → en 2 other → e

let d1 Δ = e1 ... dn Δ = en in e

Postfix Operators:

The relative precedence of two operators is unspecified if their ranges overlap. Prefix Operators:

Infix Operators:

Modules Naturals, Integers, Reals:

+ -

Modules Sequences:

\circ Head SelectSeq SubSeq Append

Modules FiniteSets:

IsFiniteSet Cardinality

Modules Bags:

Modules RealTime:

RTBound RTnow now

Modules TLC:

:> @@ Print Assert JavaTime SortSeq