Where clause in inductive

Stream: lean4

[Marcus Rossel]

Is it possible to use a where clause in an inductive definition?
I'm defining some propositions inductively, where the types of the constructors' parameters are somewhat long propositions:

inductive partialExec (σ₁ σ₂ : Reactor ι υ) (remIn remOut : List ι) : Prop
  | small (_ :
      ∃ (l : List ι),
        remIn = l ++ remOut ∧
        σ₁ -[l]→ σ₂
    )
  | big (_ :
      ∃ (σₘ : Reactor ι υ) (π : PrecGraph σₘ) (l : List ι),
        σ₁ -[remIn]→ σₘ ∧
        π.isAcyclic ∧
        (l ++ remOut).isCompleteTopoOver π ∧
        σₘ -[l]→ σ₂
    )

Can I use a where clause as to write something like: ?

inductive partialExec (σ₁ σ₂ : Reactor ι υ) (remIn remOut : List ι) : Prop
  | small (_ : small σ₁ σ₂ remIn remOut)
  | big (_ : big σ₁ σ₂ remIn remOut)
where
  small : (σ₁ σ₂ : Reactor ι υ) (remIn remOut : List ι) : Prop := ...
  big : (σ₁ σ₂ : Reactor ι υ) (remIn remOut : List ι) : Prop := ...

---

I don't want to extract small and big into their own definitions. The whole reason I'm using an inductive definition, is to get a disjunction with named cases.

[Mario Carneiro]

I don't want to extract small and big into their own definitions. The whole reason I'm using an inductive definition, is to get a disjunction with named cases.

I'm confused, because with that where you have essentially done exactly that

[Mario Carneiro]

Although, if the main declaration was a def, the name of the auxiliaries created by where would be partialExec.small and partialExec.big, and in this case that will collide with the names of the constructors

[Mario Carneiro]

What do you expect the final, compiled type of partialExec.small (the constructor) to look like?

[Marcus Rossel]

Mario Carneiro said:

I don't want to extract small and big into their own definitions. The whole reason I'm using an inductive definition, is to get a disjunction with named cases.

I'm confused, because with that where you have essentially done exactly that

True. I guess what's bothering me is purely the aesthetic look of the constructors. I find them quite awkward, so I was hoping to be able to adjust the syntax.

[Reid Barton]

Any reason you don't break up those arguments into three/seven separate fields for the constructors?