Coding level of the constructible hierarchy (source code)

= Coding level of the constructible hierarchy

A level $L_\lambda$ is a coding level when $\lambda$ is a <limit ordinal>, the representation of every <well-order code> in $L_\lambda$ is below $\lambda$, and every <ordinal> below $\lambda$ has a well-order code in $L_\lambda$.