how to import an inductive type

Stream: new members

[Frank Dai]

namespace foo
inductive A : Type
| a : A
end foo

open foo (A)
#check A -- this works
#check A.a -- this fails

How do I get A such that A.a is in scope too?

[Shing Tak Lam]

namespace foo
inductive A : Type
| a : A
end foo

open foo

#check A
#check A.a

[Bryan Gin-ge Chen]

(deleted)

[Jalex Stark]

(same answer as @Shing Tak Lam )

[Frank Dai]

I have other things in foo which conflict with the current scope

[Jalex Stark]

make another namespace?

[Jalex Stark]

do some renaming?

[Frank Dai]

making a namespace worked, I had a section and not a namespace

[Jalex Stark]

(i don't understand your last comment)

[Jalex Stark]

namespace foo
inductive A : Type
| a : A
end foo

#check foo.A
#check foo.A.a

[Bryan Gin-ge Chen]

If you don't want to open everything in foo, you can also do this:

namespace foo
inductive A : Type
| a : A
end foo

open foo (A) (A.a)
#check A -- this works
#check A.a -- this works

[Frank Dai]

My code was actually

namespace foo
end foo

section bar
open foo
-- name conflicts galore
end bar

changing section bar to namespace bar worked