Missing Data.Nat.Base and Data.List.Base in the 2.4.2.1 branch about agda-stdlib HOT 6 CLOSED

I'm doing this now and documenting also which modules can be considered basic as well given their dependencies. By doing so, I realize that Relation.Nullary.Core has no purpose anymore. Indeed Relation.Nullary only depends on Relation.Nullary.Core and thus it cannot introduce a cycle to fuse them. Because of the policy on .Core modules it means we can safely drop it, right?

from agda-stdlib.

Also if the user is not suppose to use the .Core module then there should be a .Base module for Char and String, which I think can safely replace the corresponding .Core modules in this case.

Comments?

from agda-stdlib.

Yes, you can remove Relation.Nullary.Core.

from agda-stdlib.

Modifications to Char and String also approved.

from agda-stdlib.

Modifications to Char and String also approved.

I'm not sure. It seems these .Core modules really exist for avoiding cycling importations.

For example, why

show : Char → String
show = primShowChar

toNat : Char → ℕ
toNat = primCharToNat

from Data.Char shouldn't be in Data.Char.Base?

from agda-stdlib.

Thanks!

from agda-stdlib.