## Stream: general

### Topic: protected and add_decl

#### 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?

#### Yury G. Kudryashov (Aug 16 2019 at 08:20):

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

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

#### Yury G. Kudryashov (Aug 16 2019 at 08:25):

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

I don't know.

#### Yury G. Kudryashov (Aug 16 2019 at 08:25):

I want to auto sync this property in to_additive

#### Mario Carneiro (Aug 16 2019 at 08:25):

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

#### Mario Carneiro (Aug 16 2019 at 08:26):

we can probably fix that in community lean

#### Yury G. Kudryashov (Aug 16 2019 at 08:34):

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

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

#### Mario Carneiro (Aug 16 2019 at 08:39):

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

#### 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

#### Yury G. Kudryashov (Aug 16 2019 at 08:41):

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

#### 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