Stream: Type theory
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?
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