4.11. Tactic.EqLift.Tactic.Unlift
Unlift tactic
This file defines the unlift_eq tactic, which performs the inverse operation of lift_eq. It
takes an equality that has been lifted to a common universe level and attempts to unlift it back to
its original form. The tactic is designed to work with various types of expressions, and can be
extended by registering new unlift functions.
Module LeanMachineLearning.Tactic.EqLift.Tactic.Unlift contains 5 exposed declarations.