2.1. At a glance🔗

Several spellings differ from the mainstream languages Laurel is a target for. They are worth skimming once, because they are the most common source of a first parse error.

Intent	Laurel syntax
Field read or write	`obj#field`, `obj#field := value`
Instance procedure call	`obj#method(args)`
Assignment	`x := value`
String concatenation	`a ^ b`
Eager Boolean and/or	`a & b`, `a \| b`
Short-circuit and/or	`a && b`, `a \|\| b`
Implication	`a ==> b`
Euclidean integer division/remainder	`a / b`, `a % b`
Truncating integer division/remainder	`a /t b`, `a %t b`
Deterministic unknown	`<?>`
Nondeterministic unknown	`<??>`
Label and jump	`{ ... } label`, `exit label`

Note that ^ is concatenation — not exponentiation, and not exclusive or. Fields use the # selector rather than the . most languages use, because . is an identifier character in Laurel and not a selector.

Three structural rules cover most of the rest:

A Laurel source file (.lr.st or .laurel.st) is a bare sequence of declarations. The program Laurel; header belongs only to #strata blocks embedded in Lean, so a standalone file must not carry it. Examples in this guide are shown without it.
Statements inside a block are separated by ;, and the final one may omit it. A procedure declaration itself always ends in ;; a composite, datatype, constrained, type, or opaque declaration does not.
Tabs are rejected as inter-token whitespace.