Zulip Chat Archive

Hi everyone,
I am next trying to port Dlist.lean (https://github.com/leanprover-community/lean3port/blob/master/Leanbin/Data/Dlist.lean) . Again this is not yet taken on #port-status
Although this is part of lean core, it seems to lie outside the Init folder. I don't see an equivalent folder inside mathlib4. Where should this file go?

Shreyas Srinivas (Dec 24 2022 at 00:01):

I noticed that this looks like something that should be in std even though it is on the mathlib4 port queue.

Eric Wieser (Dec 25 2022 at 14:06):

I think the default is to port to mathlib unless someone's says otherwise. It can always be moved to std4 later

Mario Carneiro (Dec 25 2022 at 14:35):

Indeed, even if it's intended for std I think these developments should go through mathlib4 first, so we can make sure it's working alright and does what it needs to.

Shreyas Srinivas said:

Although this is part of lean core, it seems to lie outside the Init folder. I don't see an equivalent folder inside mathlib4. Where should this file go?

Mathlib.Data.DList

Shreyas Srinivas (Dec 25 2022 at 14:58):

This clashes with the data.dlist inside mathlib https://github.com/leanprover-community/mathlib/tree/master/src/data/dlist

Mario Carneiro (Dec 25 2022 at 14:58):

That's not a file

Shreyas Srinivas (Dec 25 2022 at 15:25):

I just checked and noticed that DList/Basic.lean has been ported. It replaces the import Data.Dlist line with import Std.Data.DList so it doesn't dlist from core anymore