Thanks, Norm, for your obligingness in this case. I think this was a special case, with a lot of arguments for and against the definitions, and the discusson was an appropriate process for quality assurance. I have the feeling that we had a tie in our argumentation, so there are no winners and no losers. I also see no danger that there will be a lot of (not necessarily needed or superfluous or even harmful) definitions will be added to (the main body of) set.mm: each request for adding such a definition should be intensively discussed (as done in this case) - the current agreement is no blank check for future cases.
Nevertheless, this special case was a good example to illustrate and substantiate the goals of set.mm. I'll start moving the material into the main body of set.mm tomorrow (evening), a fine tuning can be performed by Github comments. This should also support the cleanup of Part 18, see https://groups.google.com/d/msg/metamath/0O19iCOc7LA/ypVqkxC_FAAJ. Alexander On Sunday, February 2, 2020 at 5:52:48 PM UTC+1, Norman Megill wrote: > > @benoit and @alexander - Thank you for your comments. Go ahead and import > semigroup (assuming no one else objects). Hopefully, though, I've > communicated my point that we don't want this to lead to flurry of shallow > definitions that people must learn, just to address a perceived difficulty > in understanding the df-* statements (that are technical definitions not > always meant to be read directly by humans). > > Norm > > On Sunday, February 2, 2020 at 11:11:27 AM UTC-5, Alexander van der Vekens > wrote: >> >> I want to comment on the following post in more detail: >> >> > .... > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f1eef383-f8a3-464a-8cd7-8fd023b73594%40googlegroups.com.
