get all lemmas in namespace

Stream: metaprogramming / tactics

[Johan Commelin]

How do I print all lemmas in a given namespace?

[Kevin Buzzard]

Does #print prefix <namespace> do it?

[Johan Commelin]

Hmm, I guess I shouldn't have said #print

[Johan Commelin]

I want to get them in a list name

[Gabriel Ebner]

I would use docs#environment.get_decls and docs#name.is_prefix_of

[Johan Commelin]

thx