\begin{syntax}
term ::= integer ; integer constant
| real ; real constant
| "true" | "false" ; Boolean constant
| "()" ; empty tuple
| qualid ; qualified identifier
| qualifier? "(" term ")" ; term in a scope
| qualifier? "begin" term "end" ; \textit{idem}
| tight-op term ; tight operator
| "{" term-field+ "}" ; record
| "{" term "with" term-field+ "}"
; record update
| term "." lqualid ; record field access
| term "[" term "]" "'"* ; collection access
| term "[" term "<-" term "]" "'"* ; collection update
| term "[" term ".." term "]" "'"* ; collection slice
| term "[" term ".." "]" "'"* ; right-open slice
| term "[" ".." term "]" "'"* ; left-open slice
| term term+ ; application
| prefix-op term ; prefix operator
| term infix-op-4 term ; infix operator 4
| term infix-op-3 term ; infix operator 3
| term infix-op-2 term ; infix operator 2
| term "at" uident ; past value
| "old" term ; initial value
| term infix-op-1 term ; infix operator 1
| ... ; continued in Fig.~\ref{fig:bnf:term2}
\
term-field ::= lqualid "=" term ";" ; field \texttt{=} value
\
qualid ::= qualifier? (lident-ext | uident) ; qualified identifier
\
lident-ext ::= lident ; lowercase identifier
| "(" ident-op ")" ; operator identifier
| "(" ident-op ")" ("_" | "'") alpha suffix* ; associated identifier
\
ident-op ::= infix-op-1 ; infix operator 1
| infix-op-2 ; infix operator 2
| infix-op-3 ; infix operator 3
| infix-op-4 ; infix operator 4
| prefix-op "_" ; prefix operator
| tight-op "_"? ; tight operator
| "[" "]" "'" * ; collection access
| "[" "<-" "]" "'"* ; collection update
| "[" "]" "'"* "<-" ; in-place update
| "[" ".." "]" "'"* ; collection slice
| "[" "_" ".." "]" "'"* ; right-open slice
| "[" ".." "_" "]" "'"* ; left-open slice %
\end{syntax}