4.6. Tactic.EqLift.Tactic.Utils🔗

Lift and Unlift utilities

This file provides utility functions for lifting and unlifting equalities.

Module LeanMachineLearning.Tactic.EqLift.Tactic.Utils contains 6 exposed declarations.

• liftMetadataDefinition · 0 deps
• finisherMetadataDefinition · 0 deps
• transformExprDefinition · 1 deps
• Lean.MVarId.nthRewriteDefinition · 0 deps
• constructProofDefinition · 2 deps
• transformEqualityDefinition · 5 deps