There are a lot of terms in the proof assistant / type theory literature that I'm either not familiar with or have an intuitive understanding of but not a definition for. I also think this type of question will be useful to future readers.

Of the ones I've asked so far, some of them like this one and this one are okay. Others like this one are not (if anyone has any advice for how to improve it; please let me know).

In the future, lots of people will have questions on what exactly different terms mean when reading answers on the site, so answers to what is an X questions will be useful.

So, what makes a good what is an X question? If you're a novice like me, how much of an explanation of your current understanding is appropriate?

Also, what makes a good what is an X answer? Are there more or less standard references we should cite?

  • $\begingroup$ @GuyCoder Maybe. The prolog tag entry is very detailed and works well as a gold standard. I don't think it makes "what is an X" questions unnecessary though, since not every term is important enough to get a tag entry. $\endgroup$ Commented Feb 12, 2022 at 23:39

1 Answer 1


My take which might make me a set with one member is that StackExchange sites are for learning. SE once evolved into a higher life form when they had documentation but then de-evolved when they killed it. They seem to have a strange attractor of quick answers only meaning no matter how they change this is what they always transition around.

So for your X AKA term, I don't look for that information in answers nor do I typically ask X questions. What I do instead is park the knowledge in the tag info. As a matter of fact one of my first goals here was to access the privilege approve tag wiki edits which needs 750 rep and I now have.

If you have access to see tag edit history you will see me on a lot of them.

Now I will not encourage anyone to just start editing tags because they can, I personally expect tags to live up to a higher standard. Just the other day JNat, a staff member, rejected ~10 of my edits.

References: What are tags, and how should I use them?


For an great example of a tag on the Proof Assistants site see: (link).

Hats off to Wno-all for that.

I just read the comments for the related question. When I wrote this answer I only used the question above for the context of the answer. I don't plan to change this answer, I am just noting for those that start at your question and work their way to here and wonder why this seems disconnected.

I also realized I used elminiation when writing the tag info for elminator My bad, edited the tag info.

  • $\begingroup$ Hm. Interesting. It did not occur to me to associate that kind of content with a tag. One thing that I frequently do is cite stack exchange questions and answers as definitions when asking a new question in order to make it self-contained. I always thought that the tag entry was supposed to be just detailed enough to let you know whether the tag is appropriate or not for your question. (Lots of tags in the math stack exchange contain explicit advice on when to use a tag compared to other more specific tags, which is not really about the subject matter itself.) $\endgroup$ Commented Feb 12, 2022 at 21:52

You must log in to answer this question.

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