Recursive inductive type conditions on its constructor

Stream: lean4

[Pavel Klimov]

I would like to be able to make restrictions on constructors which is allowed to use in constructors. Description is confusing, but here is example

inductive Node
| leaf
| node (children : List Node)
| leafsOnly (leafs : List Node) (onlyLeafs : (leafs.all fun x => match x with | .leaf => true | _ => false) = true )

But it doesn't work. Why I want it? Well, actual type has about 7 constructors, and predicate (restriction) should allow only 3 of them. I could split this inductive type into two, and inside "superset" inductive type make dedicated constructor for "subset". But I want to avoid it.

Why it doesn't work? Is there a way to achieve what I want without splitting my type into two or more types?

[Aaron Liu]

this is either an inductive inductive type or an inductive recursive type (I don't know enough type theory to tell which one) and Lean's type theory doesn't support either

[Aaron Liu]

it should be possible to instead do it without the restriction and then restrict all at once after the inductive is finished being defined with a docs#Subtype

[Pavel Klimov]

Ok. Thanks. Will try subtype approach.

[Jovan Gerbscheid]

By the way, x matches .leaf is an abbreviation for match x with | .leaf => true | _ => false