review on iset.mm seq theorems

25 views
Skip to first unread message

Jim Kingdon

unread,
Apr 30, 2022, 1:48:26 PMApr 30
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.


Alexander van der Vekens

unread,
May 1, 2022, 1:39:54 PMMay 1
to Metamath
There are currently two PRs: #2584 and #2588. How are they related? I just reviewed #2588 (and have some remarks...).

Jim Kingdon

unread,
May 1, 2022, 6:13:24 PMMay 1
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.

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