Zulip Chat Archive

Stream: general

Topic: noob question about pexpr

view this post on Zulip Paul-Nicolas Madelaine (Jun 12 2019 at 14:49):

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?

view this post on Zulip Floris van Doorn (Jun 12 2019 at 17:27):


view this post on Zulip Floris van Doorn (Jun 12 2019 at 17:30):


view this post on Zulip Floris van Doorn (Jun 12 2019 at 17:30):

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

view this post on Zulip Floris van Doorn (Jun 12 2019 at 17:36):

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.

view this post on Zulip Mario Carneiro (Jun 12 2019 at 22:18):

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

view this post on Zulip Scott Morrison (Jun 12 2019 at 23:10):

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

view this post on Zulip Paul-Nicolas Madelaine (Jun 13 2019 at 09:40):

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

Last updated: May 14 2021 at 00:42 UTC