4.7. Tactic.EqLift.Tactic.Universe
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. -
getUniverseFromEq: extracts the universe level from the left-hand side of an equality expression.
Module LeanMachineLearning.Tactic.EqLift.Tactic.Universe contains 4 exposed declarations.