3
$\begingroup$

I'm asking questions about certain type-checking phases of a proof assistant (conversion-check, elaboration, pretty-printing, unification, etc.). Should I add tags for those? There is another way to do it, which is to use the tag , but I'm not sure if it's encouraged.

$\endgroup$
4
  • 2
    $\begingroup$ When in doubt add a tag. I assure you if the community is not in favor of such you will get feedback. $\endgroup$
    – Guy Coder
    Apr 29, 2022 at 10:52
  • $\begingroup$ I would just be careful with some of those tags, if you mean them for use with just implementation then I would hyphenate the tag with implementation. For many those would nice tags to use out side of implementation, but for those specifically interested in implementing a prover from the ground up, reading tens to hundreds incorrectly tagged items becomes a pain. $\endgroup$
    – Guy Coder
    Apr 29, 2022 at 10:55
  • $\begingroup$ @GuyCoder See my answer for why I think it is not a good idea to hyphenate tags in this way $\endgroup$
    – Couchy Mod
    Apr 29, 2022 at 15:13
  • 1
    $\begingroup$ To be clear, there is no problem with hyphenating pretty-printing, but with hypenation like coq-unification, lean-implementation etc. $\endgroup$
    – Eric Mod
    Apr 30, 2022 at 18:34

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .