let v = t in β¦πβ§ \(\mathbf{let}\;v = t\;\mathbf{in}\;\varphi\) — Explicit Substitution / Let-Binding Operator (let..in, AST Constructor: ELet)
Explicit substitution binder let v = t in β¦πβ§ binding variable v to value t inside π (Entry DefMetaInstantiation (4.01)).
| Field | Mathematical & Kernel Specification (MKTD1 / MKTD2) |
|---|---|
| Symbol |
let v = t in β¦πβ§
\(\mathbf{let}\;v = t\;\mathbf{in}\;\varphi\)
|
| Category | Binder (Explicit Substitution Operator) |
| SML AST Constructor | ELet of (UCol * UCol * 'a * 'b LBound_id) [in datatype EXP, typetheory.ML:804] |
| Constructor Arguments | 1. Bound variable v : Variable; 2. Substituend term t : A; 3. Body expression π : B |
| Metatype / Signature | (v : Variable) Γ (t : A) Γ B β B |
| Binder Status | YES β Explicit Substitution Binder (let v = t in π) |
| Defining Kernel Entries (ML Labels) | See Related Symbols & Kernel Entries below. |
| LaTeX Form | \mathbf{let}\;v = t\;\mathbf{in}\;\varphi |
| How to Understand It | SML AST Constructor: |
| Canonical Law / Usage | β(v:Variable)((π, G β’ βΉlet β¦vβ¦ = β¦tβ§ in β¦πβ§βΊ) β· (π, G β’ β¦β¦vβ¦ β tβ¦π)) |
| Related Symbols & Kernel Entries |