Zulip Chat Archive

Stream: new members

Topic: how to import an inductive type


view this post on Zulip Frank Dai (May 18 2020 at 03:24):

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?

view this post on Zulip Shing Tak Lam (May 18 2020 at 03:28):

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

open foo

#check A
#check A.a

view this post on Zulip Bryan Gin-ge Chen (May 18 2020 at 03:28):

(deleted)

view this post on Zulip Jalex Stark (May 18 2020 at 03:29):

(same answer as @Shing Tak Lam )

view this post on Zulip Frank Dai (May 18 2020 at 03:29):

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

view this post on Zulip Jalex Stark (May 18 2020 at 03:30):

make another namespace?

view this post on Zulip Jalex Stark (May 18 2020 at 03:30):

do some renaming?

view this post on Zulip Frank Dai (May 18 2020 at 03:31):

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

view this post on Zulip Jalex Stark (May 18 2020 at 03:31):

(i don't understand your last comment)

view this post on Zulip Jalex Stark (May 18 2020 at 03:31):

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

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

view this post on Zulip Bryan Gin-ge Chen (May 18 2020 at 03:32):

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

view this post on Zulip Frank Dai (May 18 2020 at 03:32):

My code was actually

namespace foo
end foo

section bar
open foo
-- name conflicts galore
end bar

changing section bar to namespace bar worked


Last updated: May 06 2021 at 21:09 UTC