I asked this question about Coq recently.

I'm curious what the correct tag would be for this type of question. In the linked question, I'm asking about the possible ways of taking a pre-existing type and creating a new type by constraining its instances to satisfy some property.

When I wrote that question specifically, I was assuming there was a bread-and-butter Coq feature that would do this (hence the dependent type tag).

Guy Coder, however, raises an interesting point.

What tag should be used for questions about how approaches for defining things within proof assistants that make proving things convenient/tractable/elegant?


1 Answer 1


How about ?

I believe the phrase "best practices" could cover features and strategies for writing code (e.g. designing data types and writing proofs) in a specific proof assistant that make proofs "convenient", "elegant", or "idiomatic".

After reading the post linked by V2Blast, I get that "best practices" is a frowned upon phrase, and therefore not the best tag here.

Not every aspect of all possible questions needs a tag. If you have your own code that works and want to ask for a better way to achieve the same thing, there's (and OP's linked question falls into this category). If you don't, it falls into a very general category of questions "How do I do X [in proof assistant Y]?" which probably doesn't need a tag of its own. (One might suggest which already exists, but I believe it is way too broad for a tag. This is a topic for another meta post though.)


You must log in to answer this question.

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