Stream: new members

Topic: term for non-inductive inductive definition?

Chris M (Sep 05 2020 at 10:57):

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 (Sep 05 2020 at 11:53):

non-recursive inductive type

Thorsten Altenkirch (Sep 05 2020 at 13:36):

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

Last updated: May 06 2021 at 21:09 UTC