4.4. Tactic.EqLift.Tactic.Kernel.KernelLift🔗

Implementation of the lift_eq tactic for kernels.

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

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

• liftCompositionDefinition · 5 deps
• liftParallelCompDefinition · 5 deps
• liftProdDefinition · 5 deps
• liftCompProdDefinition · 5 deps
• liftIdDefinition · 3 deps
• liftDiscardDefinition · 3 deps
• liftCopyDefinition · 3 deps
• liftSwapDefinition · 2 deps
• liftKernelDefinition · 2 deps
• finisherKernelLiftDefinition · 2 deps