term for non-inductive inductive definition?

Stream: new members

[Chris M]

A terminological question: What do we call an "inductive definition that doesn't use induction", such as :

inductive sum (α : Type u) (β : Type v)
| inl {} (a : α) : sum
| inr {} (b : β) : sum

Something like "non-recursive inductive type"? It's a bit clunky.

[Mario Carneiro]

non-recursive inductive type

[Thorsten Altenkirch]

It is a sum or a coproduct to be precise a labelled sum or a labelled coproduct