I accepted already https://github.com/metamath/set.mm/pull/3731, and I think it is a good idea to generalize the theorems for Words requiring the same alphabet at the moment. So please go on ...
[email protected] schrieb am Mittwoch, 3. Januar 2024 um 23:15:38 UTC+1: > On Monday, January 1, 2024 at 4:16:59 PM UTC-7 David A. Wheeler wrote: > > It looks great! I see several people already reviewed it, all liked it, > and it's already been merged. So I think you have your answer :-). > > This is exactly the process we like! Propose things incrementally so it's > easier to review the change, tweak it where appopriate, merge, repeat. > Thanks so much. > > > Well, PR #2 is going to be delayed a bit. I am tackling ccatlen next. > It is used in more proofs than eqwrd, and I have a brand new time crunch > that is going to keep me busy for about a week. I'm about 3/4 of the way > through fixing up consuming proofs, so hopefully I can have something to > show early next week. > -- > Jerry James > -- 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/9a2afaf7-d4f7-4eaa-8a2e-619ed91463d0n%40googlegroups.com.
