λ \(\lambda\) — Function & Family Abstraction Binder (λ, AST Constructor: EFun / Class Lambda)
Variable-binding abstraction operator λ(x:A). t(x) constructing a class-family (ThmFamilyEvaluation (3.37)) or dependent function in Π(x:A), B(x) (DefSigmaModel (3.38)).
| Field | Mathematical & Kernel Specification (MKTD1 / MKTD2) |
|---|---|
| Symbol |
λ
\(\lambda\)
|
| Category | Binder (Function / Family Abstraction) |
| SML AST Constructor | EFun of (UCol * 'a LBound_id) [in datatype EXP, typetheory.ML:802] |
| Constructor Arguments | 1. Domain type A : UCol; 2. Bound variable x : Variable; 3. Body term t(x) |
| Metatype / Signature | (Variable : A) × B(x) → (Π(x:A), B(x)) |
| Binder Status | YES — Function / Class-Family Abstraction Binder |
| Defining Kernel Entries (ML Labels) | See Related Symbols & Kernel Entries below. |
| LaTeX Form | \lambda |
| How to Understand It | SML AST Constructor: |
| Canonical Law / Usage | (λ(x:Class). t(x))(a) = t(a) |
| Related Symbols & Kernel Entries |