Pure type systems and let-expressions

I can not find any simple and detailed source of how to add non-recursive let-expressions to pure type systems.

The best I found is the Henk paper by Simon Peyton Jones, but his explanation of this point is very brief.

Can someone link some references about this topic (source code is accepted)?

EDIT

The let I want to add has the following syntax:

let x : T = M in N

where x is the variable name, T is its type, M is the expression with which all free occurrences of x in expression N will be replaced. It can only introduce nested definitions, so recursion is impossible.

In untyped lambda calculus it is syntactic sugar. By analogy it should be equivalent to (λ(x : T) -> N) M, but as you know this conversion does not type-check in PTS, so new type rules must be included.

There is a definite dearth of literature on how to add let bindings to PTSes or dependently typed systems, though I do seem to recall this reference:

Paolo Severi, Pure Type Systems with Definitions.

From a theoretical perspective, you want to have the intuitive rule:

$$\frac{\Gamma\vdash t[M/x] : A[M/x]\qquad \Gamma\vdash M:B}{\Gamma\vdash\mbox{let}\ x :B :=M\ \mbox{in}\ t\ :\ A} $$

But this doesn't help explain much about how to perform type checking and conversion, which is a quite subtle subject.

StackExchange Computer Science Q#93738, answer score: 4