@[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.BaseRuleSetMember Aesop.BaseRuleSet

structure Aesop.DeclaredRuleSets : Type

Structure containing information about all declared Aesop rule sets.

• ruleSets : Lean.HashMap Aesop.RuleSetName (Aesop.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 : Lean.HashSet Aesop.RuleSetName

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

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 × Lean.Name × Lean.Name))

Equations

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

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

Equations

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