Zulip Chat Archive

Stream: mathlib4

Topic: Kleisli(Cat)

Adam Topaz (Jan 01 2023 at 21:22):

I just noticed that category_theory.category.Kleisli appears on the port status page but it seems to have already been ported.

Reid Barton (Jan 01 2023 at 21:22):

I think that's one of the files that I tried to fix the source headers for a few days ago

Adam Topaz (Jan 01 2023 at 21:23):

The header on the ported file seems fine?

Adam Topaz (Jan 01 2023 at 21:24):

https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/CategoryTheory/Category/KleisliCat.lean for reference

Reid Barton (Jan 01 2023 at 21:24):

Aha, the capitalization appears to be wrong

Reid Barton (Jan 01 2023 at 21:24):

of the lean 3 module name

Adam Topaz (Jan 01 2023 at 21:24):

Aha!

Adam Topaz (Jan 01 2023 at 21:25):

would you like to open a PR with a fix?

Reid Barton (Jan 01 2023 at 21:26):

If someone else would like to, that would be even better

Adam Topaz (Jan 01 2023 at 21:27):

I can do it... give me a few mins

Adam Topaz (Jan 01 2023 at 21:27):

I assume it's just kleisli -> Kleisli, or is there another typo?

Adam Topaz (Jan 01 2023 at 21:30):

mathlib4#1290

Riccardo Brasca (Jan 02 2023 at 11:30):

Also Combinatorics/Quiver/Symmetric.lean appears to be ported but is not on the list. I think because the header says

This file was ported from Lean 3 source module combinatorics.quiver.connected_component

Riccardo Brasca (Jan 02 2023 at 11:32):

mathlib4#1297

Matej Penciak (Jan 02 2023 at 18:05):

Riccardo Brasca said:

Also Combinatorics/Quiver/Symmetric.lean appears to be ported but is not on the list. I think because the header says
This file was ported from Lean 3 source module combinatorics.quiver.connected_component

Thanks! I put the header in by hand after the fact incorrectly, and I was confused about why it didn't fix the port status page displaying it as unported

Last updated: Dec 20 2023 at 11:08 UTC