Zulip Chat Archive

Stream: mathlib4

Topic: Order.SuccPred.Relation

Niels Voss (Jan 02 2023 at 02:01):

I'm working on porting Order.SuccPred.Relation to mathlib4. After about 10 mins, I currently have the file compiling with no warnings since very few changes were required from what Mathport generated. However, I can't push my changes to GitHub because this is my first port and I don't have permission. Should I push to my own fork and PR from there? My GitHub username is osbourn.

Yaël Dillies (Jan 02 2023 at 06:08):

@maintainers :point_up:

Johan Commelin (Jan 02 2023 at 08:40):

@Niels Voss Voila: https://github.com/leanprover-community/mathlib4/invitations

Niels Voss (Jan 02 2023 at 08:42):

Thank you!

Kevin Buzzard (Jan 02 2023 at 13:51):

Thanks a lot @Niels Voss and welcome aboard!

Last updated: Dec 20 2023 at 11:08 UTC