@[reducible, inline]

abbrev Aesop.RuleSetExtension : Type

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

Equations

• Aesop.RuleSetExtension = Lean.SimpleScopedEnvExtension Aesop.BaseRuleSetMember Aesop.BaseRuleSet

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.

def Aesop.instInhabitedDeclaredRuleSets.default : DeclaredRuleSets

Equations

• Aesop.instInhabitedDeclaredRuleSets.default = { ruleSets := default, defaultRuleSets := default }

@[implicit_reducible]

instance Aesop.instInhabitedDeclaredRuleSets : Inhabited DeclaredRuleSets

Equations

• Aesop.instInhabitedDeclaredRuleSets = { default := Aesop.instInhabitedDeclaredRuleSets.default }

@[implicit_reducible]

instance Aesop.instEmptyCollectionDeclaredRuleSets : EmptyCollection DeclaredRuleSets

Equations

• Aesop.instEmptyCollectionDeclaredRuleSets = { emptyCollection := { ruleSets := ∅, defaultRuleSets := ∅ } }

opaque Aesop.declaredRuleSetsRef : IO.Ref DeclaredRuleSets

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

Equations

• Aesop.getDeclaredRuleSets = do let __do_lift ← ST.Ref.get Aesop.declaredRuleSetsRef pure __do_lift.ruleSets

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

Equations

• Aesop.getDefaultRuleSetNames = do let __do_lift ← ST.Ref.get Aesop.declaredRuleSetsRef pure __do_lift.defaultRuleSets