Questions tagged [discussion]
Use if the question you're asking is designed to reflect different opinions or best-practices on a particular topic, with the goal of reaching community consensus.
61
questions
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 ...
TreborMod
- 4,025
4
votes
1
answer
50
views
Where do we define and keep track of the scope of the site
I recently voted to close What is known about minimal sets of axioms?, because I think it would be better suited for (say) maths.SE.
The close vote options are:
This question does not appear to be ...
- 2,300
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 ...
- 3,095
4
votes
1
answer
68
views
Policies on answers porting code
In questions such as this, the OP asks for proofs, definitions, methodology etc. on a specific topic, but does not require a specific proof assistant*. There will imaginably be answers that are purely ...
TreborMod
- 4,025
4
votes
2
answers
107
views
Should we allow Rosetta-Stone style questions?
This question was raised in the comments of this question about idiomatic ways to prove the associativity of append.
A Rosetta Stone style question would describe some kind of task in a prover-neutral ...
- 3,095
5
votes
0
answers
103
views
Making / keeping the site expert friendly
I'm a novice at this subject. There are many questions I could ask that are pretty basic. These sorts of questions may have some benefit to future readers, since getting a critical mass of knowledge ...
- 3,095
5
votes
1
answer
70
views
Should "Proof Assistants for Vim Users" be made community wiki?
A while ago I asked a question about information regarding vim support for various proof assistants.
As I've had answers come in, I've started wondering if we should make it community wiki, since I ...
- 329
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 ...
- 9,195
4
votes
1
answer
38
views
Is it possible to transfer my questions from other SE sites? [duplicate]
I have ~20 questions on Stack Overflow about Isabelle and Coq. Most of them (probably all of them) would be better suited here, and were only posted on SO because I had no better SE site to post to.
I ...
- 101
6
votes
1
answer
59
views
Good "What is an X" questions & good answers to them
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 ...
- 3,095
6
votes
2
answers
160
views
Why is a question about dependent type theory off topic?
The question Elimination rule for identity types in Martin-Lof Type Theory [closed] was recently closed for being off-topic.
While I agree it should have been closed for being a duplicate, I don't see ...
- 2,300
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; ...
- 3,200
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?
- 238
13
votes
2
answers
182
views
Is this for assistants only, excluding automated provers?
Do automated theorem provers fall under the scope of this new Stack Exchange sub-site, as well as Proof Assistants?
- 519
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 ...
- 373