{ x | ๐ } / ฮบ \(\{ x \mid \varphi \} \;/\; \kappa\) — Class Comprehension Binder ({ x | ๐ }, AST Constructor: CpKappa)
The primitive class comprehension binder { x | ๐ } (also denoted ฮบ) forms the class of all sets x : Class satisfying syntactic formula ๐ : Fm. All three tokens {, |, and } in a comprehension expression resolve to this single binder symbol.
| Field | Mathematical & Kernel Specification (MKTD1 / MKTD2) |
|---|---|
| Symbol |
{ x | ๐ } / ฮบ
\(\{ x \mid \varphi \} \;/\; \kappa\)
|
| Category | Binder (Class-Forming Variable-Binding Functional Symbol) |
| SML AST Constructor | HC (CpKappa of 'Class_Truth_FUNEX) [in datatype Class_p, typetheory.ML:554] |
| Constructor Arguments | 1. Bound variable x : Variable (default type Class, never Set); 2. Formula matrix ๐ : Fm (= Bool.Expression) |
| Metatype / Signature | (Variable ร Fm) โ Class.Expression | Semantically: (Class โ Bool) โ Class |
| Binder Status | YES โ Variable-Binding Class-Forming Functional Symbol (Binder). All three tokens '{', '|', and '}' in { x | ๐ } link to this single symbol page. |
| Defining Kernel Entries (ML Labels) | Inference Rule RulClassComprehension (3.01): Class comprehension (#RulClassComprehension / #label-class-comprehension) |
| LaTeX Form | \{ x \mid \varphi \} \;/\; \kappa |
| How to Understand It | Kernel AST & Logical Specification of Class Comprehension:
|
| Canonical Law / Usage | โ(k:Class.Expression)โ(x:Name)โ(๐:Fm)(FFI(k,โนxโบ,๐) โ ((โฆkโง โ {โฆxโฆ|โฆ๐โง}) โท ((โฆkโง set) โง (let โนxโบ = โฆkโง in โฆ๐โง)))) |
| Related Symbols & Kernel Entries |
Defining Axioms, Rules & Formal Definitions (Rendered Directly from Kernel Entries)
Generated without code duplication by invoking render_entry_row_base "../manual.html" on the corresponding kernel Entry records.
| # | Formal Entity Specification | ||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 3.01 |
|