Data.Part

Stream: mathlib4

[Moritz Doll]

I was looking at Data.Part, which should be ok to port, but there is a big part (no pun intended) that relies on the tidy tactic and also cc is used in several places. Does it hurt if I start porting what is doable at the moment and let the PR sleep until the tidy tactic is there?

[Kevin Buzzard]

You can use tidy? in lean 3 and see if that proof ports, and make a porting note. I thought aesop was Lean 4 for tidy? I should think that letting a PR sleep is acceptable iff the PR is about an important file, otherwise people will want to work around problems, get the file ported, and maybe come back later.

[Kevin Buzzard]

simp breaking and being worked around is something I think we should be a little concerned about, but tidy and cc not existing and so some proofs being replaced by more low level ones (with a porting note saying what's going on) isn't the end of the world at all.

[Scott Morrison]

aesop is pretty awesome, and I'd encourage you to try it out in places where tidy is used in mathlib3.

[Scott Morrison]

You can find a little bit of example of customising aesop in the CategoryTheory folder. So far we're pretty much just using it out of the box.