LeanMachineLearning

4.16. Tactic.KernelHom.Tactic.HomKernel🔗

hom_kernel tactic

This file implements the hom_kernel tactic, the inverse of kernel_hom. It transforms equalities written in the monoidal category back into equivalent equalities of kernels.

Main declarations

  • transformHomToKernel: recursive translation from categorical morphism expressions to kernel expressions.

  • applyHomKernel: core implementation on goals and hypotheses.

  • hom_kernel: user-facing tactic (with location support).

Module LeanMachineLearning.Tactic.KernelHom.Tactic.HomKernel contains 10 exposed declarations.