Contributing definition of greedoids

Stream: mathlib4

[Jihoon Hyun]

I'd like to improve my draft on greedoids https://github.com/leanprover-community/mathlib4/blob/greedoid-defs/Mathlib%2FData%2FGreedoid%2FBasic.lean I'm currently writing on the phone so I can't explain about it much, but I am keep proving lemma and propositions when I have spare time. I'd like to get advice on what I should fix and work on to actually contribute to mathlib, aside from documentation. (Maybe tactic or naming ideas?)

[Kevin Buzzard]

Start by taking a chunk of <= 150 lines and making a PR. You may well get feedback that way. It's much harder to give feedback on thousands of lines of code because it's hard to even know where to start.

[Jihoon Hyun]

I made a pull request which contain two files which have < 200 loc, and is a small subset of the working version.

[Kevin Buzzard]

This is still a very big PR (around 300 lines in total). Why not just start with the predefs file and remove the other file (just delete it from the PR and explain that it's coming next)? You will find that the community has a lot to say about your work.

[Jihoon Hyun]

@Kevin Buzzard Cleaned up!