Union of two types?

Stream: new members

[Vivek Rajesh Joshi]

structure ReducedRow0 (n : Nat)

structure ReducedRown0 (n : Nat) where
  z : Fin n
  k : Nat
  tail : Vector F k
  h : n = p + k + 1

I want to define a type whose elements could be of either ReducedRow0 type or ReducedRown0 type. Both are mutually disjoint. How do I do so? Is there a better way than making a new inductive type that has both of these as constructors?

[Henrik Böving]

There is also the Sum type which already is the type you are looking for but generally speaking no beyond having an inductive there is no way

[Vivek Rajesh Joshi]

The problem with the inductive type is this:

inductive ReducedRow
| ReducedRow0
| ReducedRown0

If row : RoeducedRow, then row = ReducedRow0 or row = ReducedRown0, as opposed to row : ReducedRow0 or row : ReducedRown0`, which is what I want.

[Vivek Rajesh Joshi]

I tried out Sum, and it's exactly what I wanted. Thanks!

[Mark Fischer]

I think you could have used an inductive if each constructor takes the appropriate type as a parameter. Maybe something like:

inductive ReducedRow (n : ℕ)
  | R0 (_ : ReducedRow0 n)
  | Rn0 (_ : ReducedRown0 n)

or written differently:

inductive ReducedRow (n : ℕ)
  | R0 : ReducedRow0 n → ReducedRow n
  | Rn0 : ReducedRown0 n → ReducedRow n