Symbol Reference: Variable — Syntactic Variable Identifier Sort (Variable, Constructor: UVariable)

Variable \(\mathsf{Variable}\) — Syntactic Variable Identifier Sort (Variable, Constructor: UVariable)

The syntactic sort Variable of variable identifiers in the kernel AST. Distinct from Class (semantic collections) and Class.Expression (syntactic class terms).

Field	Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol	Variable \(\mathsf{Variable}\)
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 (Variable Identifiers)`
Binder Status	See Category & Signature above
Defining Kernel Entries (ML Labels)	See Related Symbols & Kernel Entries below.
LaTeX Form	`\mathsf{Variable}`
How to Understand It	SML AST Constructor: `OpConstructor UVariable` (`TVariable`) in `typetheory.ML`. A metavariable `v : Variable` is a variable-name variable (or variable variable), whereas `x : Class` is a class variable.
Canonical Law / Usage	`(x : Variable)`
Related Symbols & Kernel Entries	Syntactic Name Sort Name Syntactic Expression Functor .Expression Alphabet Variables Reference