Zulip Chat Archive

Stream: general

Topic: mk_local_const : name -> pexpr?


Zesen Qian (Jul 09 2018 at 21:25):

Is there such a function that give a pexpr of local constant from the variable name? I can just call expr.local_const, but the constructor is kind of complex and not so much documentation, also I don't think it's the way to go.

Mario Carneiro (Jul 10 2018 at 00:30):

There is mk_const, but one way or another you have to decide what to do about universe variables

Zesen Qian (Jul 10 2018 at 00:39):

sorry, what's the difference between const and local_const? also, I'm trying to work without the tactic monad.

Mario Carneiro (Jul 10 2018 at 00:41):

const is a global constant, which is declared by a def or theorem or axiom, like nat or nat.succ or nat.succ_pos

Mario Carneiro (Jul 10 2018 at 00:42):

local_const is a "local constant" which is probably less than helpful but you would usually think of it as a variable. These are the variables that appear in the context during a tactic proof, left of the turnstile

Zesen Qian (Jul 10 2018 at 00:42):

ahh I see.

Zesen Qian (Jul 10 2018 at 00:43):

yeah, so I guess I'm trying to create a reference to local constant, from a string.

Mario Carneiro (Jul 10 2018 at 00:43):

This is in contrast to var which is a de bruijn variable, which are variables which are currently bound in a binder in a term

Zesen Qian (Jul 10 2018 at 00:43):

I can create name by mk_simple_name, but from that to expr I don't know.

Mario Carneiro (Jul 10 2018 at 00:44):

You can't make a local constant from a string without the local context

Mario Carneiro (Jul 10 2018 at 00:44):

that is what enables name resolution

Zesen Qian (Jul 10 2018 at 00:44):

ok, so I need to be in a tactic.

Zesen Qian (Jul 10 2018 at 00:44):

monad.

Mario Carneiro (Jul 10 2018 at 00:44):

right

Mario Carneiro (Jul 10 2018 at 00:45):

you want get_local I think

Zesen Qian (Jul 10 2018 at 00:45):

yes, I saw that.

Zesen Qian (Jul 10 2018 at 00:45):

and I was wondering why it's implemented in VM, if it can be implemented natively.

Zesen Qian (Jul 10 2018 at 00:45):

and now I know why.

Mario Carneiro (Jul 10 2018 at 00:46):

You need that local context information to find out the unique name and type given the pp name

Mario Carneiro (Jul 10 2018 at 00:46):

this is what the tactic_state provides

Zesen Qian (Jul 10 2018 at 00:48):

ok. question: can I make a elet, getting a local_const, and pass it to the rest of the function, without access tactic state?

Mario Carneiro (Jul 10 2018 at 00:49):

Possibly, what are the inputs? You need a variable, a type, a value and a body

Zesen Qian (Jul 10 2018 at 00:50):

I want to construct a proof, which start with let v = ..., and I hope to get a expr refering to this v, and pass it to the rest of the proof generation.

Zesen Qian (Jul 10 2018 at 00:50):

is that viable?

Mario Carneiro (Jul 10 2018 at 00:58):

There are two ways you could proceed: you could construct the body containing v as a local_const, and then abstract it when you are finished, or you could construct it with v already abstracted, meaning you refer to it only as var 0

Mario Carneiro (Jul 10 2018 at 01:00):

Lean is mostly geared toward constructing terms the first way, particularly if you intend for the expression to be constructed partially using tactics, with a metavariable in the middle etc. Most tactics only work on "closed terms", meaning that var is not allowed

Mario Carneiro (Jul 10 2018 at 01:00):

But if you can construct the entire expr in one go with no intervention then the second approach is possible

Zesen Qian (Jul 10 2018 at 01:04):

thanks, I'll try

Zesen Qian (Jul 10 2018 at 01:04):

very much appreciated.

Sebastian Ullrich (Jul 10 2018 at 07:48):

Please also note https://github.com/leanprover/lean/issues/1921#issuecomment-363028776. This distinction between "pure" and "tactic" local constants will likely vanish in Lean 4. As well as the name "local constant".

Simon Hudon (Jul 10 2018 at 16:02):

Do you mean that this kind of type won't leak through into the Lean code?


Last updated: Dec 20 2023 at 11:08 UTC