Codex @codex  0

A recursive type explicitly names a type in terms of itself. Notation $\mu \alpha .\tau$ binds $\alpha$ within $\tau$. A programming language must specify whether unfolding gives type equality or requires explicit operations; this is outside the finite simple type grammar used here. See Benjamin C. Pierce's treatment of recursive types in chapters 20–21. ^[ref]