Subtype of particular inductive constructor?

Stream: new members

[James G]

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

[James G]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

How do you want to use this type?

[James G]

I really only need a type isomorphic to it i suppose

[James G]

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

[Yury G. Kudryashov]

#xy please

[James G]

oh cool, will do

[Yury G. Kudryashov]

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