Zulip Chat Archive

Stream: general

Topic: protected and add_decl


view this post on Zulip Yury G. Kudryashov (Aug 16 2019 at 08:17):

Hi, is it possible to make a new declaration created with add_decl protected? private? Given a name, is it possible to find out whether the corresponding declaration is public/protected/private?

view this post on Zulip Yury G. Kudryashov (Aug 16 2019 at 08:20):

BTW, what is the difference between protected and private in Lean?

view this post on Zulip Chris Hughes (Aug 16 2019 at 08:22):

protected means you can't refer to it without the namespace, i.e. you have to write foo.bar even if you have foo open. private means that you cannot use that lemma outside of that file (or possibly section or something like that).

view this post on Zulip Yury G. Kudryashov (Aug 16 2019 at 08:25):

@Chris Hughes Can I mark a new decl created with add_decl as protected?

view this post on Zulip Chris Hughes (Aug 16 2019 at 08:25):

I don't know.

view this post on Zulip Yury G. Kudryashov (Aug 16 2019 at 08:25):

I want to auto sync this property in to_additive

view this post on Zulip Mario Carneiro (Aug 16 2019 at 08:25):

if there isn't an obvious option, I would guess the answer is no

view this post on Zulip Mario Carneiro (Aug 16 2019 at 08:26):

we can probably fix that in community lean

view this post on Zulip Yury G. Kudryashov (Aug 16 2019 at 08:34):

Do you plan to drop support for lean-3.4 in mathlib anytime soon?

view this post on Zulip Yury G. Kudryashov (Aug 16 2019 at 08:36):

If no, then I couldn't use this feature even if it was implemented in the community lean.

view this post on Zulip Mario Carneiro (Aug 16 2019 at 08:39):

meh, I think we are just waiting for a reason to break backward compatibility

view this post on Zulip Mario Carneiro (Aug 16 2019 at 08:39):

it's sort of a chicken and egg problem if fixes aren't made because of this

view this post on Zulip Yury G. Kudryashov (Aug 16 2019 at 08:41):

Then I should make it compile at my computer (Fedora 30)

view this post on Zulip Kevin Buzzard (Aug 16 2019 at 14:25):

My undergraduates do lots of random one off projects that aren't destined for mathlib -- some of them don't have a clue which version of lean they're running. They just run the one I install on their laptops and never upgrade. They don't have to do any maintenance and it just works. They would be candidate users for lean 3.5. for me the main thing is simply that they engage with Lean


Last updated: May 10 2021 at 00:31 UTC