This language has the simply-typed lambda calculus as its host language, with extensions adding new syntax. Note we do not define evaluation in this language. The let and pair extensions are based on the example language in "Sound type-dependent syntactic language extension".
let construct that can split a pair