Symbol Reference: ⟦ ... ⟧ — White Square Brackets (Binder Scope, Explicit Substitution & Semantic Valuation Val

⟦ ... ⟧ \(\llbracket \dots \rrbracket\) — White Square Brackets (Binder Scope, Explicit Substitution & Semantic Valuation Val_ρ)

Delimits bound variable scopes in class comprehension and binders (⟦x:Class | 𝛂(x)⟧), explicit substitution 𝛂⟦x ↤ t⟧, and semantic valuation ⟦e⟧_ρ = Val_ρ(e) under assignment ρ.

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 Valuation (A.Expression → A)`
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 for two well-typed purposes: 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 Valuation (`⟦e⟧_ρ = Val_ρ(e)`): Evaluating a syntactic expression `e : Class.Expression` (or formula `𝛂 : Truth.Expression`) to its semantic denotation in `Class` (or `Bool`) under a variable assignment `ρ : Variable → Class` (distinct from syntactic splicing `⟨ ... ⟩` inside quotation).
Canonical Law / Usage	`⟦x:Class \| 𝛂(x)⟧`
Related Symbols & Kernel Entries	Metalevel Braces ⦃ ... ⦄ and ⟪ ... ⟫ Expression Translation μ_A & Valuation μ_ρ Inference Rule RulClassComprehension (3.01): Class comprehension Axiom AxmMetaClassComprehension (4.06): Class comprehension axiom schema(meta,WIP)