How can I evaluate variables under Tactic Mode?

Stream: Is there code for X?

[yichi zhou]

Hi guys. I know evaluate variables is usually easy. But when I'm trying to evaluate the value in tactic mode. Lean complains unknown identifier. What should I do? Below is the code

theorem Dummy : 1=1 := by
let a := 1 + 1
#eval a

[Eric Wieser]

What do you mean by "evaluate variables is normally easy"? I'm pretty sure it's normally impossible!

[Kevin Buzzard]

It's certainly easier if you're not in tactic mode!

[Kyle Miller]

It seems like it should be possible to make an #eval e tactic that

1. sees which fvars that e depends on
2. throw an error if any of these fvars isn't a local let definition
3. create e' from e using mkLetFVars
4. run the normal #eval algorithm on this e' and report the result

[yichi zhou]

Hi, Kyle. Thank you very much for your suggestion! I'm trying to follow your suggestion. But it turned out to be not easy for me, as I'm a new hand at lean and some APIs are not introduced in the book of meta programming. Could you please tell me how can I learn to use these APIs?