4.15. Tactic.KernelHom.Tactic.Delaborators
Delaborators for simplified kernel presentations
This file implements delaborators that provide simplified pretty-printing kernel-related
categorical operations that are generated using the kernel_hom tactic.
To use these delaborators, simply open the KernelHom namespace.
Module LeanMachineLearning.Tactic.KernelHom.Tactic.Delaborators contains 4 exposed declarations.