Symbol Reference: ⟦ ... ⟧ — White Square Brackets (Binder Scope, Denotation & Explicit Substitution)

⟦ ... ⟧ \(\llbracket \dots \rrbracket\) — White Square Brackets (Binder Scope, Denotation & Explicit Substitution)

Delimits bound variable scopes in class comprehension and binders (⟦x:Class | 𝛂(x)⟧), explicit substitution 𝛂⟦x ↤ t⟧, and semantic evaluation.

Field	Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol	⟦ ... ⟧ \(\llbracket \dots \rrbracket\)
Category	Binders, Scopes & Substitution
SML AST Constructor	`Kernel AST Symbol / Sort Constructor in typetheory.ML (Class_p / Truth_p / EXP / UCol)`
Constructor Arguments	Typed arguments as specified by the Signature / Sort field above
Metatype / Signature	`Binder Scope / Explicit Substitution / Semantic Denotation Bracket`
Binder Status	See Category & Signature above
Defining Kernel Entries (ML Labels)	See Related Symbols & Kernel Entries below.
LaTeX Form	`\llbracket \dots \rrbracket`
How to Understand It	The double white square brackets `⟦ ... ⟧` (Unicode U+27E6 / U+27E7) are used in the Obelisk Proof Assistant whenever a syntactic construct needs unambiguous meta-level grouping distinct from ordinary term parentheses `( ... )`: Binder & Comprehension Scopes: Delimiting the body of universal/existential quantifiers, class comprehensions, and operator bindings so nested parentheses inside terms never collide with binder boundaries. Semantic Denotation / Evaluation: Representing the semantic interpretation `⟦e⟧_A = μ_A(e)` of a syntactic expression `e` under valuation `A`.
Canonical Law / Usage	`⟦x:Class \| 𝛂(x)⟧`
Related Symbols & Kernel Entries	Metalevel Braces ⦃ ... ⦄ and ⟪ ... ⟫ Term Interpretation / Valuation μ_A Inference Rule RulClassComprehension (3.01): Class comprehension Axiom AxmMetaClassComprehension (4.06): Class comprehension axiom schema(meta,WIP)