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.

  • nextIdx : Nat

    Counter for generating new (normalized) universe parameter names.

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

  • paramNames : Array Lake.Name

    Parameters that have been normalized.

State for the universe level normalizer monad.

Instances For
    @[inline, reducible]

    Monad for the universe leve normalizer

    Instances For

      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.

      Instances For

        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.

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

        Instances For