Universe level utilities

This file provides utilities for working with universe levels in metaprograms. It includes conversion functions between levels and syntax, and universe level collection.

Main declarations

• collectExprUniverses: recursively collects universe levels from expressions.
• collectEqUniverses: collects the universe levels of both sides of an equality.
• getUniverseFromEq: extracts the universe level from the left-hand side of an equality expression.

def collectExprUniverses.aux (e : Lean.Expr) : List Lean.Level

Recursively traverses an expression and collects all universe levels.

Equations

• collectExprUniverses.aux (Lean.Expr.const declName univs) = univs
• collectExprUniverses.aux (Lean.Expr.sort u) = [u]
• collectExprUniverses.aux (f.app a) = collectExprUniverses.aux f ++ collectExprUniverses.aux a
• collectExprUniverses.aux (Lean.Expr.lam binderName t b binderInfo) = collectExprUniverses.aux t ++ collectExprUniverses.aux b
• collectExprUniverses.aux (Lean.Expr.forallE binderName t b binderInfo) = collectExprUniverses.aux t ++ collectExprUniverses.aux b
• collectExprUniverses.aux (Lean.Expr.letE declName t v b nondep) = collectExprUniverses.aux t ++ collectExprUniverses.aux v ++ collectExprUniverses.aux b
• collectExprUniverses.aux (Lean.Expr.mdata data b) = collectExprUniverses.aux b
• collectExprUniverses.aux (Lean.Expr.proj typeName idx b) = collectExprUniverses.aux b
• collectExprUniverses.aux (Lean.Expr.bvar deBruijnIndex) = []
• collectExprUniverses.aux (Lean.Expr.fvar fvarId) = []
• collectExprUniverses.aux (Lean.Expr.mvar mvarId) = []
• collectExprUniverses.aux (Lean.Expr.lit a) = []

def collectExprUniverses (e : Lean.Expr) : Lean.MetaM (List Lean.Level)

Recursively traverse an expression and collect universe levels found. Returns a list of all unique universe levels encountered.

Equations

• collectExprUniverses e = do let e ← Lean.instantiateMVars e let e ← Lean.Meta.zetaReduce e pure (collectExprUniverses.aux e).eraseDups

def collectEqUniverses (eq : Lean.Expr) : Lean.MetaM (List Lean.Level)

Collect the universe levels of both sides of an equality and of their type. The Eq constant itself is skipped: its level is the sort of the type of the equality, which is one universe above the terms.

Equations

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

def computeMaxLevel (levels : List Lean.Level) : Lean.MetaM Lean.Level

Compute the maximum universe level from a list of levels. The result is normalized, so that the universe levels of the lifted expressions stay small and readable (e.g. max u v instead of max (max u v) (max u v)).

Equations

• computeMaxLevel [] = Lean.throwError (Lean.toMessageData "Expected at least one universe level, got an empty list.")
• computeMaxLevel (head :: tail) = pure (List.foldl Lean.Level.max head tail).normalize

def getLevelFromEq (eq : Lean.Expr) : Lean.MetaM Lean.Level

Extract the universe level from the left side of an equality expression.

Equations

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