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

Equations

• Aesop.Frontend.extensionDescr rsName = { name := rsName, addEntry := fun (rs : Aesop.BaseRuleSet) (r : Aesop.BaseRuleSetMember) => rs.add r, initial := ∅ }

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

Equations

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

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

Equations

• Aesop.Frontend.isRuleSetDeclared rsName = do let __do_lift ← Aesop.getDeclaredRuleSets pure (__do_lift.contains rsName)

def Aesop.Frontend.checkRuleSetNotDeclared {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT IO m] (rsName : 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 : 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] [MonadLiftT Lean.CoreM m] (rsName : RuleSetName) : m (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 : RuleSetExtension) (simpExt : Lean.Meta.SimpExtension) (simprocExt : Lean.Meta.Simp.SimprocExtension) : m GlobalRuleSet

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Aesop.Frontend.getDefaultGlobalRuleSets = do let __do_lift ← liftM Aesop.getDefaultRuleSetNames Aesop.Frontend.getGlobalRuleSets __do_lift.toArray

def Aesop.Frontend.getDeclaredGlobalRuleSets : Lean.CoreM (Array (RuleSetName × 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] [MonadLiftT Lean.CoreM m] [Lean.MonadEnv m] {α : Type} (rsName : RuleSetName) (f : GlobalRuleSet → α × GlobalRuleSet) : m α

Equations

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

def Aesop.Frontend.modifyGlobalRuleSet (rsName : RuleSetName) (f : GlobalRuleSet → 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] [MonadLiftT Lean.CoreM m] [Lean.MonadEnv m] [Lean.MonadResolveName m] (rsName : RuleSetName) (r : 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] [MonadLiftT Lean.CoreM m] [Lean.MonadEnv m] (rsf : RuleSetNameFilter) (rf : RuleFilter) (checkExists : Bool) : m Unit

Equations

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