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)?
let I want to add has the following syntax:
let x : T = M in N
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.