4.5. Tactic.EqLift.Tactic.Lift🔗

Lift tactic

This file defines the lift_eq tactic, which lifts an equality to a common universe level. It propagates the lifting through the structure of the equality. The tactic is implemented in a way that it can be easily extended to support new types of expressions by registering new lifting functions.

Module LeanMachineLearning.Tactic.EqLift.Tactic.Lift contains 7 exposed declarations.

• registerLiftExprDefinition · 1 deps
• registerLiftFinisherDefinition · 1 deps
• liftExprDefinition · 2 deps
• getMaxLvlDefinition · 3 deps
• liftEqualityDefinition · 10 deps
• liftEqualityWithLevelDefinition · 9 deps
• EqLiftDefinition · 0 deps