What does export do in Lean3

Stream: mathlib4

[Chris Hughes]

I'm trying to port model_theory/syntax. below the definition docs#first_order.language.term there is the line export term. What does this do and how do I port it to Lean4?

[Yaël Dillies]

It's like a perpetual open language (term). Not sure how to translate it.

[Adam Topaz]

https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html?highlight=export

[Adam Topaz]

And this suggests that it should work in lean4 as well: https://leanprover.github.io/theorem_proving_in_lean4/interacting_with_lean.html?highlight=export#more-on-namespaces

[Adam Topaz]

This works:

inductive Foo where | bar : Nat → Foo
--#check bar <-- error
export Foo (bar)
#check bar --<-- no error

[Chris Hughes]

Thanks

[Kevin Buzzard]

import category_theory.abelian.basic

namespace category_theory

export nat (succ)

#check succ -- succ : ℕ → ℕ

end category_theory

-- #check succ -- fails
-- #check category_theory.succ -- fails as well

open category_theory

#check succ -- succ : ℕ → ℕ

what a funny thing! I never knew you could do that.

[Yaël Dillies]

Oh, I knew it could do that, but I never considered whether we should. @Violeta Hernández, what do you think of export order (succ) in the namespace ordinal?

[Violeta Hernández]

Seems useful

[Violeta Hernández]

I think that's the only thing we use from that namespace