De Bruijn indexing for inductive types

Stream: Type theory

[Roman Bars]

De Bruijn indexing allows us to avoid naming the bound variables in lambda terms. But when we define inductive types we need to name the constructors (e.g. 0:N, succ:N->N). Is there an analogous way to number the constructors of inductive types to avoid naming them?

[Eric Wieser]

Inductive constructors are global, so there's no real point numbering them. Having said that, the Lean 3 C ++ API just assigns the constructors sequential integers from 0.