Zulip Chat Archive

Stream: mathlib4

Topic: alias & protected


Yury G. Kudryashov (Jan 21 2023 at 00:48):

Is it hard to allow lemmas created by alias to be protected? @Mario Carneiro @Gabriel Ebner

Mario Carneiro (Jan 21 2023 at 00:53):

The hard part is coming up with syntax for it

Gabriel Ebner (Jan 21 2023 at 00:54):

alias already accepts docstrings, why not extend that to decl modifiers?

Gabriel Ebner (Jan 21 2023 at 00:54):

We could also add a @[protected] attribute to make it easier to set the protected flag manually.

Mario Carneiro (Jan 21 2023 at 01:07):

Is there a structural reason we can't have protected as an attribute?

Gabriel Ebner (Jan 21 2023 at 01:11):

No there's no reason at all. We can make protected an attribute today.

Mario Carneiro (Jan 21 2023 at 01:16):

can we eliminate protected-the-modifier?

Mario Carneiro (Jan 21 2023 at 01:17):

TBH I think it makes more sense as an attribute to begin with

Gabriel Ebner (Jan 21 2023 at 01:27):

Why not both?

Gabriel Ebner (Jan 21 2023 at 01:28):

We also have both add_decl_doc and juxtaposition.

Eric Wieser (Feb 11 2023 at 16:36):

This came up again here

Eric Wieser (Apr 01 2023 at 09:15):

And here, cc @Yaël Dillies


Last updated: Dec 20 2023 at 11:08 UTC