Zulip Chat Archive

Stream: new members

Topic: Subtype of particular inductive constructor?


view this post on Zulip James G (May 16 2020 at 22:56):

Is there an easier way to define a subtype for a particular inductive constructor than {o : option α // option.is_some o}?

view this post on Zulip James G (May 16 2020 at 22:58):

(using options as an example, but say if i've got a bunch more variants)

view this post on Zulip Yury G. Kudryashov (May 16 2020 at 23:02):

Do you need a subtype or a type isomorphic to this subtype?

view this post on Zulip Yury G. Kudryashov (May 16 2020 at 23:03):

How do you want to use this type?

view this post on Zulip James G (May 16 2020 at 23:04):

I really only need a type isomorphic to it i suppose

view this post on Zulip James G (May 16 2020 at 23:06):

i'd like to build a second inductive and require that some of its arguments are particular variants of the first inductive

view this post on Zulip Yury G. Kudryashov (May 16 2020 at 23:06):

#xy please

view this post on Zulip James G (May 16 2020 at 23:06):

oh cool, will do

view this post on Zulip Yury G. Kudryashov (May 16 2020 at 23:08):

Why not make the second inductive take arguments of these constructors and apply the constructors as needed?


Last updated: May 13 2021 at 21:12 UTC