# Documentation

Lean.Compiler.LCNF.Level

# Universe level utilities for the code generator #

## Universe level parameter normalizer #

The specializer creates "keys" for a function specialization. The key is an expression containing the function being specialized and the argument values used for the specialization. The key does not contain free variables, and function parameter names are irrelevant due to alpha equivalence. The universe level normalizer ensures the universe parameter names are irrelevant when comparing keys.

• Counter for generating new (normalized) universe parameter names.

nextIdx : Nat
• Mapping from existing universe parameter names to the new ones.

• Parameters that have been normalized.

paramNames :

State for the universe level normalizer monad.

Instances For
@[inline]

Monad for the universe leve normalizer

Equations

Normalize universe level parameter names in the given universe level.

Normalize universe level parameter names in the given expression.

Normalize universe level parameter names in the given expression. The function also returns the list of universe level parameter names that have been normalized.

Equations
• One or more equations did not get rendered due to their size.

## Universe level collector #

This module extends support for Code. See Lean.Util.CollectLevelParams.lean

In the code specializer, we create new auxiliary declarations and the universe level parameter collector is used to setup the new auxiliary declarations.

See Decl.setLevelParams.

@[inline]
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations

Collect universe level parameters collecting in the type, parameters, and value, and then set decl.levelParams with the resulting value.

Equations
• One or more equations did not get rendered due to their size.