4.19. Tactic.KernelHom.Tactic.KernelCat
Kernel category tactics
This file implements the kernel_coherence and kernel_monoidal tactics, which apply the
kernel_hom transformation and then use categorical coherence or monoidal tactics to solve the
resulting goal.
Main declarations
-
kernel_coherence: tactic combining kernel_hom and categorical coherence. -
kernel_monoidal: tactic combining kernel_hom and categorical monoidal coherence.
Module LeanMachineLearning.Tactic.KernelHom.Tactic.KernelCat contains 3 exposed declarations.