All Questions
Tagged with discussion tags
11
questions
4
votes
0
answers
26
views
On tags for technical support
I doubt that tags like installation is of any use. No one is probably going to watch or use this tag, because people don't tend to learn everything about the installation of every proof assistant.
I ...
4
votes
0
answers
38
views
Renaming "extensional-equality" to "extensional-type-theory"
Is there any better suggestion or reasons against changing extensional-equality to extensional-type-theory? As Couchy suggests, the current tag is slightly ambiguous. If there is no objection, I think ...
4
votes
0
answers
40
views
How to write a tag wiki excerpt?
I'm hoping to establish some sort of guideline for writing tag wiki excerpts (or usage guidance).
Examples of tag wiki excerpts I find usually fall into two categories. The first references the tag ...
2
votes
0
answers
27
views
Tags concerning variables and bindings
Should the tags bound-variables binders (and possibly de-bruijn-indexing) be merged? There probably won't be any question exclusively discussing binders and not bound variables. De bruijn indices, in ...
4
votes
1
answer
66
views
Tag for questions about definitions and approach
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 ...
6
votes
1
answer
111
views
Not correct to say that lean community is mostly mathematicians
I noticed Guy Coder made a number of edits to a lot of tags. I accepted them all since overall they were much better, but on the same time in a number of them he suggested that lean (especially Lean ...
15
votes
1
answer
117
views
Low-quality tags
There are some tags that I don't think are really necessary. They look like someone wanted to come up with more tags that would apply to their question and just lifted some words from the question; ...
9
votes
1
answer
68
views
Does [theorem-proving] need to exist?
I think the theorem-proving tag should be deleted, because it is too general - almost every question will be related to theorem proving. Should it be deleted?
11
votes
1
answer
64
views
Should there be a mathlib tag for Lean?
There are already a number of questions that are specifically about the monolithic math library mathlib created in Lean. Should we have these kinds of tags ...
4
votes
0
answers
20
views
Tags for Isabelle Locales and Classes
I believe having a locales for Isabelle will help with organizing questions. I have added Tag info but it is still pending in peer review.
Now the main question is about this question which is ...
6
votes
2
answers
67
views
Removing the [recommendations] tag
There is a recommendations tag on Proof Assistants.
Should this be deleted, as it encourages opinion-based answers?