in (let v = t in e) \(\mathbf{in}\) — Body Delimiter of Explicit Substitution Binder (let v = t in e, AST Constructor: ELet)
Keyword in separating the variable binding v = t from the body expression in let v = t in e (Entry DefMetaInstantiation (4.01)). Note: set membership is always written with the Unicode symbol ∈ (symbols/in-pred.html).
| Field | Mathematical & Kernel Specification (MKTD1 / MKTD2) |
|---|---|
| Symbol |
in (let v = t in e)
\(\mathbf{in}\)
|
| Category | Binder Delimiter (Part of Explicit Substitution ELet) |
| SML AST Constructor | ELet of (UCol * UCol * 'a * 'b LBound_id) [in datatype EXP, typetheory.ML:804] |
| Constructor Arguments | Delimiter separating binding v = t from body 𝛗 in let v = t in 𝛗 |
| Metatype / Signature | (v : Variable) × (t : A) × B → B |
| Binder Status | YES — Part of Explicit Substitution Binder (ELet) |
| Defining Kernel Entries (ML Labels) | See Related Symbols & Kernel Entries below. |
| LaTeX Form | \mathbf{in} |
| How to Understand It | SML AST Constructor: Part of |
| Canonical Law / Usage | let v = t in 𝛗 |
| Related Symbols & Kernel Entries |