Thanks! I have replied in github, hopefully we can figure out what to do
about the issues raised there.
Not too late if anyone else wants to take a look or ask any questions.
I'm always game for talking about iset.mm and even though there might
still be things to do with the recursion theorem and/or "seq", I'm
pretty excited about making progress on some longstanding annoyances.
As for the two pull requests, there is now just a combined one at
https://github.com/metamath/set.mm/pull/2588 so hopefully that removes
any confusion about that.
On May 1, 2022 10:39:54 AM PDT, 'Alexander van der Vekens' via Metamath
<[email protected]> wrote:
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 <http://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/415c35b3-1177-217a-5866-61656ed00b57%40panix.com.
