@[inline, reducible]

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.RuleSetMember Aesop.RuleSet

structure Aesop.DeclaredRuleSets : Type

Structure containing information about all declared Aesop rule sets.

• ruleSets : Lean.HashMap Lean.Name Aesop.RuleSetExtension
• defaultRuleSets : Lean.NameSet

instance Aesop.instInhabitedDeclaredRuleSets : Inhabited Aesop.DeclaredRuleSets

Equations

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

instance Aesop.instEmptyCollectionDeclaredRuleSets : EmptyCollection Aesop.DeclaredRuleSets

Equations

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

opaque Aesop.declaredRuleSetsRef : IO.Ref Aesop.DeclaredRuleSets

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

Equations

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

def Aesop.getDefaultRuleSetNames : IO Lean.NameSet

Equations

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