@[reducible, inline]

abbrev Aesop.RuleSetExtension : Type

An environment extension containing an Aesop rule set. Each rule set has its own extension.

structure Aesop.DeclaredRuleSets : Type

Structure containing information about all declared Aesop rule sets.

• ruleSets : Std.HashMap RuleSetName (RuleSetExtension × Lean.Name × Lean.Name)

  The collection of declared rule sets. Each rule set has an extension, the name of the associated SimpExtension and the name of the associated SimprocExtension. The two simp extensions are expected to be declared.

• defaultRuleSets : Std.HashSet RuleSetName

  The set of Aesop rule sets that are enabled by default.

instance Aesop.instInhabitedDeclaredRuleSets : Inhabited DeclaredRuleSets

instance Aesop.instEmptyCollectionDeclaredRuleSets : EmptyCollection DeclaredRuleSets

opaque Aesop.declaredRuleSetsRef : IO.Ref DeclaredRuleSets

def Aesop.getDeclaredRuleSets : IO (Std.HashMap RuleSetName (RuleSetExtension × Lean.Name × Lean.Name))

def Aesop.getDefaultRuleSetNames : IO (Std.HashSet Lean.Name)