Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: get all lemmas in namespace


view this post on Zulip Johan Commelin (Oct 28 2020 at 07:50):

How do I print all lemmas in a given namespace?

view this post on Zulip Kevin Buzzard (Oct 28 2020 at 07:54):

Does #print prefix <namespace> do it?

view this post on Zulip Johan Commelin (Oct 28 2020 at 08:01):

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

view this post on Zulip Johan Commelin (Oct 28 2020 at 08:01):

I want to get them in a list name

view this post on Zulip Gabriel Ebner (Oct 28 2020 at 08:22):

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

view this post on Zulip Johan Commelin (Oct 28 2020 at 08:44):

thx


Last updated: May 09 2021 at 21:10 UTC