"Often performed as the first step in an automated theorem prover"

The world is really big, I can't believe there are enough automated theorem provers out there to use the word "often"

Amazing

@Rojo hello

@Mr.Wizard Hey!

The weird behaviour is still there!

If I define _[___, up, ___] ^= "UpValue";

then just by evaluating "up" I get "UpValue" as output

Does that happen to you too?

@Rojo Yes.

Do you know why?

I konw that when I wrote the answer, I think it was bringing me problems greater than that small thing

but perhaps it was simply driving me crazy and confusing me but bringing no problems, not sure

Well, _[___, up, ___] is terribly aggressive, which is what prompted my question in the first place. Only HoldComplete[up] or Hold[{up}] etc. work. I think that the UpValue evaluates during output formatting. This got my while trying to use TracePrint if you recall.

If[False,up,With[{OutputSizeLimit`Dump`boxes$=Block[{$RecursionLimit=Typeset`$Re‌​cursionLimit},MakeBoxes[up,StandardForm]]},OutputSizeLimit`Dump`loadSizeCountRule‌​s[];If[TrueQ[BoxForm`SizeCount[OutputSizeLimit`Dump`boxes$,1048576]],OutputSizeLi‌​mit`Dump`boxes$,OutputSizeLimit`Dump`encapsulateOutput[up,$Line,$SessionID,5]]],u‌​p]

You are right

That's what's evaluated that was giving me trouble

So you say we delete the If thing from the question?

answer

Agreed. Obviously this definition should not be used in practice; it was simply to create a worst-case scenario.

Ok, deleted it

Regarding editing the answer would you be amenable to writing it with terse symbol (pattern) names as I did mine, or is that not your style?

I merely ask because the condensed form is a thing of beauty to me. :-)

@Mr.Wizard You mean short pattern names?

@Mr.Wizard I am not sure I understood but it's fastest if you edit and I understand it from the edit. Feel free

I just meant this:

SetAttributes[f, HoldAllComplete];

f[args___] :=
  Module[{x},
   x /: {x, rest___} := HoldComplete[rest];
   {x, args}
  ]

With this it becomes apparent that your method is more compact than mine, in addition to cleaner which was already apparent.

I thought "first" was more meaningful as to the importance of it being the first

Actually, ^:= should work here I believe.

@Rojo Ah, interesting point.

but it can become shorted ir I don't localize x's definition. But you don't like that, right?

@Rojo That depends on the way an answer is presented. If it's simply to illustrate a method then localization is not needed. (e.g. here) Other times it would be very easy to create leaks, such as when doing f[x_] = D[ . . ., x] and IMHO localization should be included in the answer.

Right

See if you like it

New edit, first will be in a context named f, a compromise between local and not

lol

fun, huh?

I give up

I like the form without (backtick)f(backtick) myself, but with ^:=.

@Mr.Wizard before you leave, any interesting performance tuning question that might still need a look? I feel like performance tuning

@Mr.Wizard Edited

lol -- this is the unformattable string :-)

`f`

Hahaha

Ah.

Hoooow

Tricky, these backticks.

The backslashes sometimes do not behave as expected...

Backslash is an escape here? Why didn't I know that. :-p

`f`first

Niiiiiiiiiiiiiiiiiiiiice

@Mr.Wizard Just like in that program we like to use. What was it called again...

\backslash