lemma full names and namespaces

Stream: general

[Yury Yarovikov]

Hey there! I've been doing some research on automated theorem proving in Lean, during which I encountered a problem: I want my machine learning model to store all the lemmas in the library and to have an ability to insert their names into generated code.
The problem is that, in Lean, lemmas are members of namespaces which, in turn, can also be members of other nested namespaces. With that in mind, I have 2 questions.