Category Theory Rule Set

This module defines the CategoryTheory Aesop rule set which is used by the aesop_cat tactic. Aesop rule sets only become visible once the file in which they're declared is imported, so we must put this declaration into its own file.

opaque mathlib.tactic.category.grind : Lean.Option Bool

Option to control whether the category theory library should use grind or aesop in the cat_disch tactic, which is widely used as an autoparameter.

opaque mathlib.tactic.category.log_grind : Lean.Option Bool

Log a message whenever the category theory discharger uses grind.

opaque mathlib.tactic.category.log_aesop : Lean.Option Bool

Log a message whenever the category theory discharger uses aesop.