Commit 2021-07-09 22:11 70320f74

View on Github →

feat(category_theory/category/Kleisli): Fix lint errors (#8244) Fixes some lint errors for this file: unused arguments, module doc, inhabited instances

Estimated changes

Modified src/category_theory/category/Kleisli.lean

modified theorem category_theory.Kleisli.comp_def

modified theorem category_theory.Kleisli.id_def

modified def category_theory.Kleisli.mk

modified def category_theory.Kleisli