Zulip Chat Archive

Stream: Type theory

Topic: De Bruijn indexing for inductive types


view this post on Zulip Roman Bars (Mar 10 2021 at 04:44):

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?

view this post on Zulip Eric Wieser (Mar 10 2021 at 09:25):

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.


Last updated: May 08 2021 at 22:13 UTC