global export

Stream: mathlib4

[Sina Hazratpour]

Is there a convenient way to export all the items in one namespace into another? Ideally we would have a syntax like export foo in the namespace bar which exports all the terms in foo to bar. It seems currently, I need to list all the terms in the bracket, namely export foo (t_1 ... t_n) where in my case n = 10 but for higher n it might make sense to have a command to export everything, and another command to exclude some exports. Would it be a good idea to add such a command?

[Floris van Doorn]

You can definitely write such a command using metaprogramming.
If we want to add this to Mathlib/Core Lean: probably not, unless there is a really compelling use case for it.

[Sina Hazratpour]

This is in the namespace CWComplex:

export RelCWComplex (pairwiseDisjoint disjoint_openCell_of_ne openCell_subset_closedCell
  cellFrontier_subset_closedCell cellFrontier_union_openCell_eq_closedCell map_zero_mem_openCell
  map_zero_mem_closedCell isCompact_closedCell isClosed_closedCell isCompact_cellFrontier
  isClosed_cellFrontier closure_openCell_eq_closedCell skeletonLT_top skeleton_top skeletonLT_mono
  skeleton_mono skeletonLT_monotone skeleton_monotone closedCell_subset_skeletonLT
  closedCell_subset_skeleton closedCell_subset_complex openCell_subset_skeletonLT
  openCell_subset_skeleton
  openCell_subset_complex cellFrontier_subset_skeletonLT cellFrontier_subset_skeleton
  cellFrontier_subset_complex iUnion_cellFrontier_subset_skeletonLT
  iUnion_cellFrontier_subset_skeleton closedCell_zero_eq_singleton openCell_zero_eq_singleton
  cellFrontier_zero_eq_empty isClosed skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ
  skeleton_union_iUnion_closedCell_eq_skeleton_succ iUnion_skeletonLT_eq_complex
  iUnion_skeleton_eq_complex eq_of_not_disjoint_openCell disjoint_skeletonLT_openCell
  disjoint_skeleton_openCell skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier
  skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier)

Does this count as as a (compelling) use case?

My would-be use case is less long but can imagine other similar cases even longer than the above.

[Floris van Doorn]

But we don't export all declarations from CWComplex to RelCWComplex. And #30131 is trying to make that use case nicer.

[Yaël Dillies]

I was the one suggesting Sina to bring this up on Zulip, because I noticed the analogy with open: export Foo (bar) is functionally the same as a persistent open Foo (bar), but open supports more syntaxes, like open Foo and open Foo hiding bar and I couldn't explain why the analogous syntax didn't exist for export.

[Yaël Dillies]

Sina's use case is #31064, to add SemiCartesianMonoidalCategory without disturbing the existing users of CartesianMonoidalCategory.

[Floris van Doorn]

I see. But I still don't see the use case.

If you literally want to export everything from SemiCartesianMonoidalCategory, then why don't you do that manually for all projections of the structure, and afterwards just don't declare anything in the namespace SemiCartesianMonoidalCategory anymore, directly do it in CartesianMonoidalCategory, even if it's really about SemiCartesianMonoidalCategory.

This doesn't work if some lemmas would be stated slightly differently in the two cases (we have this when working with CWComplex/RelCWComplex), but it seems to work fine in this case(?)