4
$\begingroup$

I saw a tag coq-definition. Should there be $\forall l\in \text{ProofAssistants}, l\text{-definition}$ tag? Should there be like coq-expression, coq-tactic, etc. tags too? I found this tag very unnecessary. I even believe that definition itself should not be a tag, because too many things can be about "definitions" and the purpose of tags should be helping to classify the question (IMHO), not to describe the question.

EDIT: I'm talking about this question

$\endgroup$

2 Answers 2

Reset to default
5
$\begingroup$

A comment on the original post says:

I originally used the tag definition because the question is about how to define a concept expressed informally, rather than how to prove something

Yet the tag info () merely defines what a Definition is in Coq. So I don't think this tag is appropriate in this instance. I think a better name for it would be formalization.

That being said, we should really ask ourselves what tags are useful for. The reasons I can come up with are:

  • helping users find possible duplicates when asking a question, and help search algorithms (google wizardry and whatnot) find content on this site
  • to track specific tags one is interested in (this isn't anywhere near problem here yet, but look for example at stackoverflow where questions barely stay on the front page for an hour)
  • as a wiki for the site

With this in mind, and even with the original intent of the tag,

  • It's unlikely that it would help detect duplicates or help algorithms find relevant answers
  • I don't see a reason someone would track (I would just track )
  • the tag wiki offers nothing of substance

While I have nothing against putting more specific tags, I think a very real danger of tags combining two concepts such as lang-foo is that it is a conjunction of two tags, leading one to believe that it is no longer necessary to tag lang and foo. But the points I made above would suggest that omitting these tags (especially lang) would alienate the question from potential answerers and future search results.

TLDR: unless lang-foo has a very useful wiki, it is better to tag lang and foo

$\endgroup$
1
$\begingroup$

As the one who created the tag the reason for creating the tag was because I felt the question needed more than jus the tags coq and beginner. Eventually questions with just those two tags will make those tags useless.

If you know of a better way to differentiate the question by adding other tags and those tags are more meaningful to all then make the change.

$\endgroup$
2
  • $\begingroup$ Personally I think the original choice to use definition was fine, and there was no need to add the coq- prefix. $\endgroup$
    – Eric Mod
    Commented Apr 30, 2022 at 18:32
  • $\begingroup$ Maybe formalization as proposed in the other answer $\endgroup$
    – ice1000 Mod
    Commented May 1, 2022 at 16:37

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .