Symbol Reference: ⟨ ... ⟩ — Explicit Syntactic Antiquotation / Splicing Brackets & Tuple Delimiters

Personal Symbol Reference Page in MKTD1 & MKTD2 (Morse-Kelley + Tarski + Dunaev) — All Personal Symbol Pages → | Full Symbol Registry →

Formula Display:
Proof Trees:

⟨ ... ⟩ \(\langle \dots \rangle\) — Explicit Syntactic Antiquotation / Splicing Brackets & Tuple Delimiters

Splices an evaluated meta-expression or class code into a quoted syntactic template ‹ ... ›; also used as structural angle brackets for pairs/tuples.

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
⟨ ... ⟩
\(\langle \dots \rangle\)
Category Quotation & Antiquotation (Reflection Layer)
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 Class → Expression (inside ‹...›) | Dependent Pair Constructor
Binder Status See Category & Signature above
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form \langle \dots \rangle
How to Understand It

In MKTD1 and MKTD2, the angle brackets ⟨ ... ⟩ serve two closely documented roles:

  1. Explicit Antiquotation (Unquotation / Splicing) inside ‹ ... ›: When writing a quoted formula ‹ ∀x:Class. ⟨𝛂(x)⟩ ›, the sub-expression inside ⟨ ... ⟩ is evaluated at the outer level and spliced into the AST being constructed. Specifically, ‹ ⟨Dec(c)⟩ › reconstructs the syntax tree coded by c.
  2. Ordered Tuple / Pair Construction: Outside quotation contexts, ⟨a, b⟩ or (x, y) denotes ordered pairing (Entry DefEmptySet (3.04) / dependent pair in Entry DefIsSetValued (3.28)).
Canonical Law / Usage ‹(𝒯 ⊢ ⟨Enc(𝛂)⟩) ⇒ 𝛂›
Related Symbols & Kernel Entries