# Combining With, If and SetDelayed

I just noticed that

With[{x = 1}, If[x == 0, 0, 1]]


returns 1 (as I expected) but

y := If[x == 0, 0, 1];
With[{x = 1}, y]


returns an unevaluated form:

If[x == 0, 0, 1]


Can someone explain what is going on?

• With makes a "literal" replacement of the instances of x that appear in the code that follows the list. When the code is y, there is "literally" no x present. So no substitution is made, and then y is evaluated, the x appears, but the replacement time is over. – Michael E2 Aug 14 '19 at 23:10
• @kglr I might suggest Block[{x = 1}, y]. @A.G., see mathematica.stackexchange.com/questions/559/… – Michael E2 Aug 14 '19 at 23:12
• For these short examples, Trace can be a good tool to use and be familiar with. Try With[{x = 1}, y] // Trace – Michael E2 Aug 14 '19 at 23:15

Mathematica is an expression rewriting language. With[{x = 1}, y] rewrites y with every x replaced by 1. With has the HoldAll attribute, so y is left unevaluated before the rewrite takes place.
But y contains no x, so the the result is simply y. Then, since y has an ownvalue, it gets rewritten as If[x == 0, 0, 1].