def Aesop.Frontend.extensionDescr (rsName : Aesop.RuleSetName) : Lean.SimpleScopedEnvExtension.Descr Aesop.RuleSetMember Aesop.RuleSet

Equations

• Aesop.Frontend.extensionDescr rsName = Lean.SimpleScopedEnvExtension.Descr.mk (fun rs r => Aesop.RuleSet.add rs r) ∅ id

def Aesop.Frontend.declareRuleSetUnchecked (rsName : Aesop.RuleSetName) : IO Unit

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.isRuleSetDeclared (rsName : Aesop.RuleSetName) : IO Bool

Equations

• Aesop.Frontend.isRuleSetDeclared rsName = do let __do_lift ← ST.Ref.get Aesop.aesopExtensionsMapRef pure (Lean.HashMap.contains __do_lift rsName)

def Aesop.Frontend.checkRuleSetNotDeclared {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT IO m] (rsName : Aesop.RuleSetName) : m Unit

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.declareRuleSet {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT IO m] (rsName : Aesop.RuleSetName) : m Unit

Equations

• Aesop.Frontend.declareRuleSet rsName = do Aesop.Frontend.checkRuleSetNotDeclared rsName liftM (Aesop.Frontend.declareRuleSetUnchecked rsName)

def Aesop.Frontend.getRuleSetExtension {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT (ST IO.RealWorld) m] (rsName : Aesop.RuleSetName) : m Aesop.RuleSetExtension

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.getRuleSet (rsName : Aesop.RuleSetName) (includeGlobalSimpTheorems : Bool) : Lean.CoreM Aesop.RuleSet

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.getRuleSets (rsNames : Array Aesop.RuleSetName) (includeGlobalSimpTheorems : Bool) : Lean.CoreM Aesop.RuleSets

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.getDefaultRuleSets (includeGlobalSimpTheorems : Bool) : Lean.CoreM Aesop.RuleSets

Equations

• Aesop.Frontend.getDefaultRuleSets includeGlobalSimpTheorems = Aesop.Frontend.getRuleSets Aesop.defaultEnabledRuleSetNames includeGlobalSimpTheorems

def Aesop.Frontend.getDefaultRuleSet (includeGlobalSimpTheorems : Bool) (options : Aesop.Options) : Lean.CoreM Aesop.RuleSet

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.getAllRuleSets (includeGlobalSimpTheorems : Bool) : Lean.CoreM Aesop.RuleSets

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.addRuleUnchecked {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT (ST IO.RealWorld) m] [Lean.MonadEnv m] [Lean.MonadResolveName m] (rsName : Aesop.RuleSetName) (r : Aesop.RuleSetMember) (kind : Lean.AttributeKind) : m Unit

Equations

• Aesop.Frontend.addRuleUnchecked rsName r kind = do let ext ← Aesop.Frontend.getRuleSetExtension rsName Lean.ScopedEnvExtension.add ext r kind

def Aesop.Frontend.addRule {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT (ST IO.RealWorld) m] [Lean.MonadEnv m] [Lean.MonadResolveName m] (rsName : Aesop.RuleSetName) (r : Aesop.RuleSetMember) (kind : Lean.AttributeKind) : m Unit

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.eraseRules {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT (ST IO.RealWorld) m] [Lean.MonadEnv m] (rsf : Aesop.RuleSetNameFilter) (rf : Aesop.RuleNameFilter) (check : Bool) : m Unit

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.eraseRules.go {m : Type → Type} [Monad m] [Lean.MonadEnv m] (rf : Aesop.RuleNameFilter) (anyErased : Bool) (ext : Aesop.RuleSetExtension) : m Bool

Equations

• One or more equations did not get rendered due to their size.