Local Constants

With[{x=x0,y=y0,},body]define local constants x, y,

Defining local constants.

Module allows you to set up local variables, to which you can assign values and then change them. Often, however, all you really need are local constants, to which you assign a value only once. The Wolfram Language With construct allows you to set up such local constants.

This defines a global value for t:
Click for copyable input
This defines a function using t as a local constant:
Click for copyable input
This uses the definition of w:
Click for copyable input
t still has its global value:
Click for copyable input

Just as in Module, the initial values you define in With are evaluated before With is executed.

The expression t+1 which gives the value of the local constant t is evaluated using the global t:
Click for copyable input

The way With[{x=x0,},body] works is to take body, and replace every occurrence of x, etc. in it by x0, etc. You can think of With as a generalization of the /. operator, suitable for application to Wolfram Language code instead of other expressions.

This replaces x with a:
Click for copyable input
After the replacement, the body of With is a=5, so a gets the global value 5:
Click for copyable input
This clears the value of a:
Click for copyable input

In some respects, With is like a special case of Module, in which each local variable is assigned a value exactly once.

One of the main reasons for using With rather than Module is that it typically makes the Wolfram Language programs you write easier to understand. In a module, if you see a local variable x at a particular point, you potentially have to trace through all of the code in the module to work out the value of x at that point. In a With construct, however, you can always find out the value of a local constant simply by looking at the initial list of values, without having to trace through specific code.

If you have several With constructs, it is always the innermost one for a particular variable that is in effect. You can mix Module and With. The general rule is that the innermost one for a particular variable is the one that is in effect.

With nested With constructs, the innermost one is always the one in effect:
Click for copyable input
You can mix Module and With constructs:
Click for copyable input
Local variables in inner constructs do not mask ones outside unless the names conflict:
Click for copyable input

Except for the question of when x and body are evaluated, With[{x=x0,},body] works essentially like body/.x->x0. However, With behaves in a special way when the expression body itself contains With or Module constructs. The main issue is to prevent the local constants in the various With constructs from conflicting with each other, or with global objects. The details of how this is done are discussed in "How Modules Work".

The y in the inner With is renamed to prevent it from conflicting with the global y:
Click for copyable input