Higher Category Theory Rule Set and Options

In this file we define the HigherCategoryTheory rule set for Aesop as well as some options for controlling custom behavior of the library.

opaque hcat.tactic.suggest : Lean.Option Bool

Option to override the suggestive behavior of hcat_disch and aesop_hcat.

opaque hcat.tactic.nonterminal : Lean.Option Bool

Option to control whether aesop_hcat runs in non-terminal mode.

opaque hcat.tactic.omega : Lean.Option Bool

Option to control whether a wrapped omega is tried as part of hcat_disch.