def Aesop.Frontend.extensionDescr (rsName : Aesop.RuleSetName) : Lean.SimpleScopedEnvExtension.Descr Aesop.BaseRuleSetMember Aesop.BaseRuleSet

Equations

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

def Aesop.Frontend.declareRuleSetUnchecked (rsName : Aesop.RuleSetName) (isDefault : Bool) : 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 ← Aesop.getDeclaredRuleSets 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) (isDefault : Bool) : m Unit

Equations

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

def Aesop.Frontend.getGlobalRuleSetData {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT IO m] (rsName : Aesop.RuleSetName) : m (Aesop.RuleSetExtension × Lean.Name × Lean.Meta.SimpExtension × Lean.Name × Lean.Meta.Simp.SimprocExtension)

Equations

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

def Aesop.Frontend.getGlobalRuleSetFromData {m : Type → Type} [Monad m] [Lean.MonadEnv m] (ext : Aesop.RuleSetExtension) (simpExt : Lean.Meta.SimpExtension) (simprocExt : Lean.Meta.Simp.SimprocExtension) : m Aesop.GlobalRuleSet

Equations

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

def Aesop.Frontend.getGlobalRuleSet (rsName : Aesop.RuleSetName) : Lean.CoreM (Aesop.GlobalRuleSet × Lean.Name × Lean.Name)

Equations

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

def Aesop.Frontend.getGlobalRuleSets (rsNames : Array Aesop.RuleSetName) : Lean.CoreM (Array (Aesop.GlobalRuleSet × Lean.Name × Lean.Name))

Equations

• Aesop.Frontend.getGlobalRuleSets rsNames = Array.mapM Aesop.Frontend.getGlobalRuleSet rsNames

def Aesop.Frontend.getDefaultGlobalRuleSets : Lean.CoreM (Array (Aesop.GlobalRuleSet × Lean.Name × Lean.Name))

Equations

• Aesop.Frontend.getDefaultGlobalRuleSets = do let __do_lift ← liftM Aesop.getDefaultRuleSetNames Aesop.Frontend.getGlobalRuleSets (Lean.HashSet.toArray __do_lift)

def Aesop.Frontend.getDeclaredGlobalRuleSets : Lean.CoreM (Array (Aesop.RuleSetName × Aesop.GlobalRuleSet × Lean.Name × Lean.Name))

Equations

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

def Aesop.Frontend.modifyGetGlobalRuleSet {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT IO m] [Lean.MonadEnv m] {α : Type} (rsName : Aesop.RuleSetName) (f : Aesop.GlobalRuleSet → α × Aesop.GlobalRuleSet) : m α

Equations

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

def Aesop.Frontend.modifyGlobalRuleSet (rsName : Aesop.RuleSetName) (f : Aesop.GlobalRuleSet → Aesop.GlobalRuleSet) : Lean.CoreM Unit

Equations

• Aesop.Frontend.modifyGlobalRuleSet rsName f = Aesop.Frontend.modifyGetGlobalRuleSet rsName fun (rs : Aesop.GlobalRuleSet) => ((), f rs)

def Aesop.Frontend.addGlobalRule {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT IO m] [Lean.MonadEnv m] [Lean.MonadResolveName m] (rsName : Aesop.RuleSetName) (r : Aesop.GlobalRuleSetMember) (kind : Lean.AttributeKind) (checkNotExists : Bool) : m Unit

Equations

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

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

Equations

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

def Aesop.Frontend.eraseGlobalRules.go {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT IO m] [Lean.MonadEnv m] (rf : Aesop.RuleNameFilter) (anyErased : Bool) (rsName : Aesop.RuleSetName) : m Bool

Equations

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