TypeTopology
TypeTopology copied to clipboard
martinescardo
Czf ind def
Okay. I've done everything Martin suggested so I will now ping @tomdjong (but please ignore until after break :))
I have now completely formalized my paper. I think the comments and structure is pretty good. The biggest remaining problem is some of my proofs are ugly and hard to follow. But I need to do some thinking about how to improve them (also adding intro/elim rules for quantifiers could help significantly so I'll wait to hear back from @ayberkt). I look forward to more feedback from @tomdjong when you are back.
@tomdjong ready for another review at your convenience. I tried to improve naming but I anticapte some more tweaks will be neccesary. Also I resolved the comment on changing S but I still haven't come up with a good name so it's NOT resolved.
@IanRay11 Could you make a separate PR with just OrderedTypes/SupLattice.lagda and OrderedTypes/SupLattice-SmallBasis.lagda please?
This will make the reviewing easier, in particular it will become much easier for @martinescardo to comment. We can then merge that first before tackling the LFP.
@IanRay11 You should give priority to this pull request over other new formalization projects.
@tomdjong I have greatly improved the state of this file. Little to no module nesting and in many cases I succesfully made modules anonymous. Please note that I intentionally left local/bound-inductive-definitions and small-presentation modules named because passing arguements in the absence of them became unruly. But if you have any suggestions for these I am open to expirementing more with making them anon. Also I believe I utilized my subset-to-family notation completely but it is possible some slipped through the cracks (also note that in some places my current syntax didn't apply although I haven't spent too much time considering the correct generalization). There a couple of problematic line lengths towards the end that I am unsure of how to handle due to inabiliy to line break.
@tomdjong I gave names to everything as suggested. Let me know if you have any improvements. I checked everything as resolved but maybe you want to review some of my decisions...
Thanks for the edits @IanRay11!
@martinescardo I'll wait for you to return from your holiday, so that you can have a look before merging (if you wish).
@ayberkt Did you want to review this as well?
I made some more small changes to comments in light of dropping the full induction principle. I agree that other reviews could be beneficial.
@tomdjong @IanRay11 Sorry I missed this earlier.
If there is no hurry, I would be happy to review this. I think I’ll have time to do that tomorrow.
@ayberkt no rush. Also, no expectations about an extremely thorough review. I would appreciate a once over and just see if anything stands out (content or style)
@tomdjong I've now looked at this and I am very happy to accept it. Please go ahead and merge it if you wish.
@ayberkt Are you happy for me to merge this, or did you wish to review as well? (If so, could you do it by Monday please?)
Thanks, @IanRay11 , for your nice contribution, and @tomdjong , for your thorough review.
Thanks to you all for helping me polish it and allowing it a home in TypeTopology!
@ayberkt Are you happy for me to merge this, or did you wish to review as well? (If so, could you do it by Monday please?)
Sorry @tomdjong and @IanRay11, I couldn’t review this when I promised and I have been travelling since. I now have time to look at this and will add my comments today (so that you can merge it tomorrow).
@IanRay11 Once you've addressed Ayberk's comments, we can get this merged. :+1:
@IanRay11 Could you please add the file with your name to OrderedTypes/index.lagda? After that I'll merge this.