LeanMachineLearning

4.17. Tactic.KernelHom.Tactic.KernelHom🔗

kernel_hom tactic

This file implements the kernel_hom tactic, which transforms equalities of kernels into equivalent equalities in the monoidal category.

Main declarations

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

  • mkKernelHomEqProof: construction of the equivalence proof used by the tactic.

  • applyKernelHom: core implementation of kernel_hom on goals and hypotheses.

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

Module LeanMachineLearning.Tactic.KernelHom.Tactic.KernelHom contains 23 exposed declarations.