Symbol Reference: Name — Syntactic Variable-Name Sort (Name)

Name \(\mathsf{Name}\) — Syntactic Variable-Name Sort (Name)

The underlying syntactic sort Name of variable name tokens lifted into Variable via IVariable_t.

Field	Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol	Name \(\mathsf{Name}\)
Category	Metatheoretic AST Sorts
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	`Syntactic Sort (Raw Variable Names)`
Binder Status	See Category & Signature above
Defining Kernel Entries (ML Labels)	See Related Symbols & Kernel Entries below.
LaTeX Form	`\mathsf{Name}`
How to Understand It	SML AST Constructor: `TName` / `IName_Expre` in `typetheory.ML`. Used in judgments such as `(x : Name)` in `RulClassComprehension`.
Canonical Law / Usage	`[(x : Name), (𝛗 : Fm)]`
Related Symbols & Kernel Entries	Inference Rule RulClassComprehension (3.01): Class comprehension Variable Sort Variable