Fetching the thing that was added using `addAndCompile`

Stream: lean4

[Andrej Bauer]

Suppose I have installed a thing with Lean.addAndCompile named cow : Name. How do I actually obtain the the object that was installed, i.e., I how do I tell the kernel "give me the object whose name is equal to the value of cow"?

[Kim Morrison]

Lean.getConstInfo is probably what you're looking for to start with.

[Andrej Bauer]

It's more likely that I want to create a quoted expressions that is essentially the name of the thing I want to lookup, and tell the kernel to "evaluate" it (I expect the kernel to complain if no such thing exists, and otherwise give me a blessed object).

[Andrej Bauer]

Maybe Lean.evalConst.

[Sebastian Ullrich]

If you want to go from a named symbolic term to a run-time value then yes. For what it's worth, the IR generation step necessary for this happens outside the kernel, and the IR is not evaluated until required such as through evalConst