Different namespace for mutual inductive types

Stream: lean4

[Raghuram]

mutual
  inductive Tree (α) where
  | node : α → TreeList α → Tree α
  inductive Hidden.TreeList (α) where
  | nil : TreeList α
  | cons : Tree α → TreeList α → TreeList α
end

#check TreeList        -- error; desirable
#check Hidden.TreeList -- works
#check Tree            -- error; undesirable
#check Hidden.Tree     -- works

Is there a way to do this so TreeList is defined in the Hidden namespace, but Tree in the current namespace?

[Alex Keizer]

You can define the mutual in the Hidden namespace, and then re-export only Tree in the current namespace.

namespace Hidden
  mutual
    inductive Tree (α) where
    | node : α → TreeList α → Tree α
    inductive TreeList (α) where
    | nil : TreeList α
    | cons : Tree α → TreeList α → TreeList α
  end
end Hidden

export Hidden (Tree)

#check TreeList        -- error; desirable
#check Hidden.TreeList -- works
#check Tree            -- works
#check Hidden.Tree     -- works

[Raghuram]

I had tried that, but that exposes the fact that it's in the Hidden namespace for every definition one wants to make and use with dot notation afterwards (after end Hidden). I guess that's not that much of a problem though.

[Raghuram]

Also this appears to be intended behaviour, because giving the inductive types two different namespaces produces an error message about conflicting namespaces.