`expr.fold` uneccesarily(?) is not defined for `pexpr`s

[khoek]

The statement of expr.fold is

meta constant expr.fold {α : Type} : expr → α → (expr → nat → α → α) → α

which prohibits folding over pexprs. Is there any good reason for this (the only thing I can think of is a possible VM representation difference?).

If not, let's change it.

[Kha]

No, I was simply too lazy

[robertylewis]

I think quite a few of the expr functions have this unnecessary restriction and should be generalized. But it takes someone knowledgeable to know which are which, or to carefully check the source to confirm.

[gebner]

Under the hood pexpr is exactly the same data structure as expr. The types are just there to help you not to confuse them (and e.g. call infer_type on a pre-expression). They have the same representation, and you can (more or less) safely cast between them. If you want to use such a function (in mathlib), just use unchecked_cast:

meta def pexpr.fold {α : Type u} : pexpr → α → (pexpr → nat → α → α) → α :=
unchecked_cast expr.fold