Stop requiring a name for Add Ring? #12891
Labels
kind: design discussion
Discussion about the design of a feature.
part: ring/field
The ring and field tactics.
The name is used for printing in Print Rings, and to generate the lemma names. After #12890 we can generate fresh lemma names even without a unique prefix.
Therefore we could provide a command
Add Ring : some_ring_theory
(in Print Rings it could say "anonymous ring with carrier ...").Does that seem useful?
The text was updated successfully, but these errors were encountered: