## Stream: new members

### Topic: Subtype of particular inductive constructor?

#### 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}?

#### James G (May 16 2020 at 22:58):

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

#### Yury G. Kudryashov (May 16 2020 at 23:02):

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

#### Yury G. Kudryashov (May 16 2020 at 23:03):

How do you want to use this type?

#### James G (May 16 2020 at 23:04):

I really only need a type isomorphic to it i suppose

#### 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