There are currently two PRs: #2584 and #2588. How are they related? I just reviewed #2588 (and have some remarks...).
On Saturday, April 30, 2022 at 7:48:26 PM UTC+2 [email protected] wrote: > Can I get a review on https://github.com/metamath/set.mm/pull/2584 ? > > I don't think there is anything especially controversial here (the > funinsn part may or may not lead to anything else, but the rest is just > the next step in the ongoing work to remove some of the conditions on > seq theorems in iset.mm), but I probably shouldn't speculate on whether > there are no comments or approvals in github yet. > > > -- 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/f2bbf5a4-3170-4b54-84e8-6434688842c3n%40googlegroups.com.
