I'd like to create the agda-stdlib
tag to add to another question, but the only way I can see is by asking a new question. Hence this one.
-
1stackoverflow.com/help/privileges/create-tags – jonrsharpe Sep 18 '20 at 7:36
-
It says "Simply enter a new tag with your question and it will be created." So as far as I understand I do have to create a new question to add a tag? Anyway, I should probably have posted this on meta, I'm sorry for the noise. – Jesper Sep 18 '20 at 7:40
-
4Pretty sure you can just edit your current one, you have the required rep. – ivarni Sep 18 '20 at 8:20
-
It's a question by someone else (who doesn't have the required reputation). – Jesper Sep 18 '20 at 9:46
-
also note: When is it appropriate to create a tag, and how does it work? – rene Sep 18 '20 at 10:29
-
2There also is tag standard-library. Isn't combining it with agda an option? – rene Sep 18 '20 at 10:34
You have two options:
- Ask a question yourself
- Edit an existing question and add the tag
I highly recommend the latter, but that works better if you have at least 2.000 reputation and can make edits without them getting supervised, since only adding a single tag might be considered too minor to push an edit into the queue. If the question can benefit from more than just a tag edit, though, then go ahead.
If no questions exist yet that could benefit from the tag, I recommend waiting until they do. Others can create the tag too if they have sufficient reputation.
If you add a new tag, don't forget to propose an excerpt and wiki for it!
-
You don't need the rep when editing one of your own questions though, right? – Gimby Sep 18 '20 at 9:12
-
1Correct, well, just the 1.5K to be allowed to edit tags, so if you've already asked a question yourself you can edit that. If you don't have sufficient reputation to add tags, you can of course involve meta to get someone else to edit it in. – Erik A Sep 18 '20 at 9:27