global `mk_fresh_name`?

Stream: general

[Daniel Donnelly]

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?

[Daniel Donnelly]

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.

[Daniel Donnelly]

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.

[Mario Carneiro]

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

[Mario Carneiro]

oh wait no, mk_fresh_name does that

[Daniel Donnelly]

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

[Daniel Donnelly]

How do you do that then?

[Mario Carneiro]

I was thinking of get_unused_name

[Daniel Donnelly]

*create a global variable named mk_fresh_name ?

[Mario Carneiro]

?

[Mario Carneiro]

You call mk_fresh_name as a tactic

[Mario Carneiro]

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

[Mario Carneiro]

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

[Daniel Donnelly]

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

[Daniel Donnelly]

E.g.

[Daniel Donnelly]

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

[Daniel Donnelly]

Doesn't work on my machine

[Daniel Donnelly]

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

[Mario Carneiro]

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

[Mario Carneiro]

most non-interactive tactics are in the tactic namespace

[Kevin Buzzard]

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.