Zulip Chat Archive

Stream: general

Topic: Add lemma to root namespace without leaving a namespace


view this post on Zulip Yury G. Kudryashov (Feb 20 2020 at 07:07):

How can I add a lemma to the root namespace without leaving the namespace block? I understand that I can define a lemma, then use alias command. Is there any more straightforward way?

view this post on Zulip Mario Carneiro (Feb 20 2020 at 07:11):

No

view this post on Zulip Mario Carneiro (Feb 20 2020 at 07:12):

More generally, any tactic can create a declaration with any name, but you can't use the def or theorem keyword to create a new lemma outside the namespace

view this post on Zulip Mario Carneiro (Feb 20 2020 at 07:14):

I guess with some user command magic you can make something that acts passably close to theorem

view this post on Zulip Mario Carneiro (Feb 20 2020 at 07:14):

but there are lots of little things that are hard to replicate, like pulling in variables from the section

view this post on Zulip Yury G. Kudryashov (Feb 20 2020 at 08:01):

Then I'll go with private lemma, alias


Last updated: May 08 2021 at 20:11 UTC