Syntax sugar (Pipe-calculus): Difference between revisions

<math>\mathsf{let}</math> is a popular construct in functional languages that declares a lexically scoped local variable. It's usual form is <math>\mathsf{let}~x = t~\mathsf{in}~u</math> which denotes binding the name <math>x</math> to the term <math>t</math> in the term <math>u</math>.  

In lambda calculus <math>\mathsf{let}</math> can be encoded as <math>(\lambda x . u)~t</math>. Applying the ''<math>\beta</math>-rule'' we get <math>u[t/x]</math>, an instance of <math>u</math> where <math>t</math> is substituted for every free occurence of <math>x</math>.