protected and add_decl

Stream: general

[Yury G. Kudryashov]

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?

[Yury G. Kudryashov]

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

[Chris Hughes]

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).

[Yury G. Kudryashov]

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

[Chris Hughes]

I don't know.

[Yury G. Kudryashov]

I want to auto sync this property in to_additive

[Mario Carneiro]

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

[Mario Carneiro]

we can probably fix that in community lean

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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