Zulip Chat Archive

Stream: general

Topic: global `mk_fresh_name`?


view this post on Zulip Daniel Donnelly (Aug 29 2019 at 02:07):

How do you do a mk_fresh_name at the file global scope in order to create a new variable name that hasn't been used?

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 02:09):

Also, I need to be able to print that name or somehow return it from Lean back to VSCode TypeScript extension (which I'm modifying), which will then forward it to BananaCats. If this can't be done yet. That is okay :) I can keep track of Bancats-created variable names on the Bancats Pyqt5 app's end.

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 02:12):

I then have regex code to generate the next greek or indexed greek / latin variable (in LaTeX) which can then be translated to Lean code.

view this post on Zulip Mario Carneiro (Aug 29 2019 at 02:37):

there is another function with a similar name that gives you globally unique names

view this post on Zulip Mario Carneiro (Aug 29 2019 at 02:39):

oh wait no, mk_fresh_name does that

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 02:39):

Would it be listed here? https://leanprover.github.io/tutorial/A1_Quick_Reference.html

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 02:39):

How do you do that then?

view this post on Zulip Mario Carneiro (Aug 29 2019 at 02:40):

I was thinking of get_unused_name

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 02:40):

*create a global variable named mk_fresh_name ?

view this post on Zulip Mario Carneiro (Aug 29 2019 at 02:40):

?

view this post on Zulip Mario Carneiro (Aug 29 2019 at 02:40):

You call mk_fresh_name as a tactic

view this post on Zulip Mario Carneiro (Aug 29 2019 at 02:40):

it's not a global variable, it's a globally unique variable name

view this post on Zulip Mario Carneiro (Aug 29 2019 at 02:41):

get_unused_name is only fresh relative to the current context and is used for making human readable local variable names

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 02:42):

I'm not seeing the helloworld example to either of those calls anywhere

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 02:43):

E.g.

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 02:43):

example (a : Prop) : a  a :=
by do n  mk_fresh_name,
intro n,
hyp  get_local n,
exact hyp

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 02:43):

Doesn't work on my machine

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 02:43):

https://leanprover.github.io/programming_in_lean/programming_in_lean.pdf (page 32)

view this post on Zulip Mario Carneiro (Aug 29 2019 at 02:44):

that's correct except you need open tactic at the start

view this post on Zulip Mario Carneiro (Aug 29 2019 at 02:45):

most non-interactive tactics are in the tactic namespace

view this post on Zulip Kevin Buzzard (Aug 29 2019 at 07:55):

Would it be listed here? https://leanprover.github.io/tutorial/A1_Quick_Reference.html

Just to note that this page describes Lean 2 not Lean 3.


Last updated: May 06 2021 at 22:13 UTC