5 略記の詳細

5.1 内包の書き方

次の左辺では \(\mathop{{\sf X}}\) が表記上無視されます。
abbr … \(\{ T \mid P \}\) ≈ \(\{ x \mid \exists \mathop{{\sf X}} ( ( P ) , x = T ) \}\)
ソース：abbr Cls（左辺の書き方は \{ $T Cls $_X | $P \}）。「$P を満たす $_X について $T を集めたもの」で、$_X は束縛する変数（x ; y のように複数も可）です。小文字の cls（\{ cls x | P \}、条件で集める）とは別の略記です。Cls は項 $T を集めます。例 \{ x + x Cls x | x ∈ |A \} は {x + x | x ∈ A}、z ∈_ \{ x + x Cls x | x ∈ |A \} は ∃ x (x ∈ |A and z = x + x) と読まれます（slash_cli で確認）。所属の書き換え方も違います。slash_cli の出力で比べると、z ∈_ \{ cls x | x ∈ |A \} は [∈ z |A]（cls は残らず、P の x に z を代入した式になる＝「-| の仕組み」の節の cvt(cls.)）、z ∈_ \{ x Cls x | x ∈ |A \} は [∃ x [and [∈ x |A] [= z x]]]（Cls は ∃ に開く）です。
次のものの左辺は特殊表記されています。\(\sum_{i\in\{0,1\}}(i+1)=3\) のような記述のための略記です（∑ などの word は別に紹介が要ります）。
abbr … \(_{ P } T\) ≈ \(\{ T \mid P \}\)
ソース：abbr -Cls（左辺の書き方は [ $T -Cls $_X | $P ]）。中身は Cls と同じクラスで、違うのは表示（上の特殊表記）だけです。例 [ x + x -Cls x | x ∈ |A ] は \{ x + x Cls x | x ∈ |A \} と同じ式に読まれます（slash_cli で確認）。standard_math/1-1.book の ⋃_ [ \{ set x \} -Cls x | x ∈ X ] が実例です。

5.2 アロー関数

アロー関数は1項関数（gram の返り値が (s,s) の値）を作ります。項に適用するには、?f (x) と同じく直後に ( 引数 ) を書きます。ソース ｢ fn x ↦ x + a ｣ ( b )、表示は \(\lceil x \mapsto x + a \rfloor ( b )\) です。｢ ｣ は半角のかぎ括弧（U+FF62・U+FF63）です。全角の「 」とは別の文字で、「 」と書くと拒否され、半角の ｢ ｣ を案内されます（旧綴り \[ \] は2026-09-30 に廃止）。
word ap（f ap (x)）は、対の集合としての関数 f に代入する別の語です。gram は (ss,s) なので、アロー関数（(s,s) の値）に書くと型が合わず Form になりません（「「ap」の引数1には集合(s)が必要ですが…」というエラー）。
\(\mapsto\) の前の v-Form を \(\bullet\) に替えられます。その際 \(\bullet \mapsto\) は略されます。
例　 \(\lceil \bullet + a \rfloor\) ≈ \(\lceil x \mapsto x + a \rfloor\)
\(\lceil \bullet \rfloor\) は恒等写像です。● が2回あれば同じ変数です：｢ fn ● + ● ｣ は x ↦ x + x（`｢ fn ● + ● ｣ ( a ) = a + a` ◀ O は -| O p; で OK＝実測）。
\(\bullet\) は入れ子では使用すべきでありませんが、必ず内側から計算されます。
例　 \(\lceil \bullet + \lceil \bullet + a \rfloor ( x ) \rfloor\) ≈ \(\lceil \bullet + ( x + a ) \rfloor\)