句読点記号を以下に示します。
= <> ~= ~<> < <= > >= + - * / -> ( ) { } [ ] " => |=> , $
識別子は、1 つの文字またはアンダースコアーに続いていくつかの文字、数字、またはアンダースコアーで 表します。 識別子の大/小文字は区別されます。
キーワードを以下に示します。キーワードを変数や関数の名前として 使用することはできません。
| and | in | real |
| Boolean | integer | sort |
| current | let | string |
| else | map | then |
| false | model | there_exists |
| filter | not | this |
| for_all | of | traverse |
| if | or | true |
| implies | over |
整数リテラルは、オプションの負符号 (-) に続いて 1 つ以上の 10 進数字で 表します。
実数リテラルは、オプションの負符号 (-) に続いて 1 つ以上の 10 進数字、小数点、および 1 つ以上の整数で 表します。
ブール・リテラルには true と false があります。
関連リテラルは、基本的には、ストリング・リテラルを 引用符の代わりに大括弧 ([]) で囲んだものです。シーケンス ¥] は終了区切り文字をエスケープします。
ストリング・リテラルは、引用符で囲まれた 文字シーケンスです。 ストリングを複数行にわたって拡張することはできません (つまり、 ストリングに、アンエスケープされた改行を含めることはできません)。サポートされる エスケープ・シーケンスを以下の表に示します。
正規表現リテラル は、 逆引用符 (`) で囲まれた文字シーケンスです。正規表現リテラル内のいくつかの文字には 特別な意味を持つものがあります。これらの文字は、円記号の後に示された場合を除いて、 特別な意味を表します。特殊文字は、.、¥、[、]、?、*、+、^、および $ です。 正規表現リテラルには、文字エスケープ・シーケンスを含めることができます。 許可されているエスケープ・シーケンスは、¥t、¥r、¥n、および ¥xdd です。 これらは、タブ、復帰、改行、および 16 進数 dd に相当する ASCII コードの文字を表します。
正規表現は再帰的な構造を持ちます。これらは、 より小さな副次式で形成されます。すべての正規表現のビルディング・ブロックは、 単一文字と一致する式です。 これらの基本式には以下の 3 つのフォームがあります。
これらのビルディング・ブロックから、 より大きな正規表現を以下のようにして形成できます。
完全な 正規表現は、^ および $ をそれぞれ使用した文字列の始めまたは終わりに固定できます。 re が正規表現である場合、^re は、re に匹敵するすべてのストリングと 一致する正規表現ですが、これらのストリングが先頭にある場合に限られます。 同様に、re$ は、re に匹敵するすべてのストリングと 一致する正規表現ですが、これらのストリングが末尾にある場合に限られます。例えば、`^[01]+` は 0 および 0110 と一致しますが、a0 や a0110 とは 一致しません。また、`[01]+$` は 0 および 0110 と一致しますが、0a や 0110a とは 一致しません。