LeanMachineLearning

4.10. Tactic.EqLift.Tactic.Kernel.KernelUnlift🔗

Implementation of the unlift_eq tactic for kernels.

This file contains functions that propagate the unlifting of lifted kernel expressions through several operators and primitives, and constructs the necessary proofs for the unlift_eq tactic.

Module LeanMachineLearning.Tactic.EqLift.Tactic.Kernel.KernelUnlift contains 10 exposed declarations.