# Argument pattern behavior for built-in symbol

I'm having troubles with this:

test1[forAll[t,x_]]:=x
test2[ForAll[t,x_]]:=x


While syntactically exact, test1 works and test2 does not:

?test1
(* test1[forAll[t,x_]]:=x *)

?test2
(* test2[x_]:=x *)


Why doesn't ?test2 output test2[ForAll[t,x_]]:=x?

Edit 2

For anyone interested - for yet unknown reasons - this and only this works as expected:

test3[ForAll[t,t_]]:=t


Edit 3

The legit working solution to non-standard evaluation traps like this is to use unambiguous pattern matching syntax that does not provide any hints to the system that this can be evaluated:

test2[(f:ForAll)[t,x_]]:=x

• Thanks for the edit. You need HoldFirst or similar attribute, otherwise it is the same as defining f[1+1]:=whatever. – Kuba Jun 27 '17 at 19:48
• @Kuba, I do not want HoldFirst for this method. I need it without HoldFirst – grandrew Jun 27 '17 at 19:51
• @Kuba, btw I just tested test3[a_+b_]:=a and it actually does work: ?test3 (* => test3[a_+b_]:=a *) – grandrew Jun 27 '17 at 20:09
• Because a_+b_ does not evaluate further while ForAll[t,x_] does, to x_. – Kuba Jun 27 '17 at 20:12
• I'm not sure why you think this is a bug. ForAll has no Options (specifically HoldFirst), and I think by default, it takes the symbol that's in the first argument and looks for it in the second argument. Compare ForAll[x_, x_^2] with ForAll[x_, y_^2]. The second evaluates to y_^2 because it has no x_ in it. – march Jun 27 '17 at 20:32

First of all, though SetDelayed (:=) has HoldAll attribute, it still evaluates its 1st argument in this case, this behavior has been discussed in this post. To be specific, when test2 is defined, the argument ForAll[t, x_] will be evaluated.

Now the question becomes

Why ForAll[t, x_] evaluates to x_?

and this has been explained in the Scope of the document of ForAll:

If the expression does not explicitly contain a variable, ForAll simplifies automatically:

ForAll[x, y == 0]
(* y == 0 *)


In your case, x_ doesn't explicitly contain t, and it's automatically simplified, while t_ explicitly contain t so it's not. (Notice the FullForm of t_ is Pattern[t, Blank[]] i.e. a function with 2 arguments whose 1st agrument is an explicit t. )

To get the desired function definition, you can make use of Unevaluated:

ClearAll@test2
test2[Unevaluated@ForAll[t, x_]] := x
DownValues@test2
(* {HoldPattern[test2[ForAll[t, x_]]] :> x} *)

test2[ForAll[t, t + t^2]]
(* t + t^2 *)


But notice this function still won't work as expected if the ForAll[…] evaluates to something else, for example:

test2[ForAll[t, x]]
(* test2[x] *)


If you want it to evaluate to x, then Unevaluated again or as mentioned in the comment above, use HoldFirst:

test2[Unevaluated@ForAll[t, x]]
(* x *)
SetAttributes[test2, HoldFirst]
test2[ForAll[t, x]]
(* x *)

• xzczd, thank you for detailed answer. Could you please elaborate on how does t_ explicitly contain t? I thought t_ is just a local pattern variable and does not explicitly state anything and could mean any expression when matched regardless of its name? – grandrew Jun 28 '17 at 7:39
• Check my edit. If you're still confused, feel free to ask. – xzczd Jun 28 '17 at 9:20
• many thanks! that makes a lot of sense and completes my understanding of how pattern matching is implemented on top of symbolic rules engine in MMA. Btw, the word "function" may add confusion and I am not sure if this is even correct for symbol Pattern (I doubt if it emits a Function in any scenario) – grandrew Jun 28 '17 at 12:42
• I think it's OK to use the word "function" to name a non-atomic expression, even if it doesn't evaluate to anything else. In mathematics we'll simply call $f(x,y)$ a function even if we know nothing about the specific function relationship represented by $f$, right? – xzczd Jun 28 '17 at 13:15