review on seq theorems

Skip to first unread message

Jim Kingdon

Apr 30, 2022, 1:48:26 PMApr 30
Can I get a review on ?

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, 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 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

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 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 so hopefully that removes any confusion about that.

Reply all
Reply to author
0 new messages