noob question about pexpr

Stream: general

[Paul-Nicolas Madelaine]

Hello everyone,

this may be a stupid question but I was reading about lean's elaborator, and I got confused about the 'pexpr' type.
if I understand correctly, an elaborated term is a term without meta variables.
but then I don't get what the 'pexpr' is, since it's defined as 'expr ff'. so as I read it, this means an unelaborated expression.
but an 'expr' may already contain meta variables, so I don't understand what the 'elaborated' argument really means.

could someone clarify this for me?

[Floris van Doorn]

(deleted)

[Floris van Doorn]

(deleted)

[Floris van Doorn]

What is the keyboard shortcut to send my message? I keep accidentally pressing it :/

[Floris van Doorn]

pexpr are pre-expressions before elaboration, basically the terms you type.
expr are expressions after (and during) elaboration.
It is true that pexprs often contain metavariables and exprs often don't, but that is not the main difference.
It is kind of a red herring that pexpr and expr are defined as the same structure in Lean, since they represent the same term very differently.

Suppose I write a = b, or equivalently eq a b in Lean. As pexpr this will be represented as app (app (const eq) (local_const a)) (local_const b) (ignoring some arguments of local_const). Here app, const and local_const are constructors of the expr structure.
However, eq also has an implicit argument (the type of a and b). After elaboration, the expression representing the same term has this implicit argument, so it becomes: app (app (app (const eq) (local_const α)) (local_const a)) (local_const b).
So a = b as a pre-expression becomes eq a b (hiding the constructors) and as expression it becomes eq α a b.

Another (related) difference is that pexpr has some additional operations exposed. For example there is a mk_explicitwhich represents the @. So if I write @eq α a b this is the expression (mk_explicit eq) α a b.

I hope that clears things up.

[Mario Carneiro]

@Floris van Doorn the command to send is either enter or ctrl-enter depending on whether "press enter to send" box is checked

[Scott Morrison]

And if "press enter to send" is checked you can use shift-enter to get a new line.

[Paul-Nicolas Madelaine]

@Floris van Doorn thank you very much, that was very clear