Skip to main content

All Questions

Tagged with
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 ...
Trebor's user avatar
  • 4,025
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 ...
Trebor's user avatar
  • 4,025
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 ...
Couchy's user avatar
  • 2,300
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 ...
Trebor's user avatar
  • 4,025
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 ...
Greg Nisbet's user avatar
  • 3,095
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 ...
Jason Rute's user avatar
  • 9,195
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; ...
Mike Shulman's user avatar
  • 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?
pxeger's user avatar
  • 238
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 ...
march's user avatar
  • 373
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 ...
Wno-all's user avatar
  • 1,128
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?
taylor.2317's user avatar
  • 1,338