review on iset.mm seq theorems
29 views
Skip to first unread message
Jim Kingdon
Apr 30, 2022, 1:48:26 PM4/30/22
to meta...@googlegroups.com
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.
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.
Alexander van der Vekens
May 1, 2022, 1:39:54 PM5/1/22
to Metamath
There are currently two PRs: #2584 and #2588. How are they related? I just reviewed #2588 (and have some remarks...).
Jim Kingdon
May 1, 2022, 6:13:24 PM5/1/22
to 'Alexander van der Vekens' via Metamath
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.
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.
Reply all
Reply to author
Forward
0 new messages