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