Documentation

Aesop.Frontend.Extension

source
def Aesop.Frontend.extensionDescr (rsName : RuleSetName) :
Lean.SimpleScopedEnvExtension.Descr BaseRuleSetMember BaseRuleSet
Instances For
    source
    def Aesop.Frontend.declareRuleSetUnchecked (rsName : RuleSetName) (isDefault : Bool) :
    IO Unit
    Instances For
      source
      def Aesop.Frontend.isRuleSetDeclared (rsName : RuleSetName) :
      IO Bool
      Instances For
        source
        def Aesop.Frontend.checkRuleSetNotDeclared {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT IO m] (rsName : RuleSetName) :
        m Unit
        Instances For
          source
          def Aesop.Frontend.declareRuleSet {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT IO m] (rsName : RuleSetName) (isDefault : Bool) :
          m Unit
          Instances For
            source
            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)
            Instances For
              source
              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
              Instances For
                source
                def Aesop.Frontend.getGlobalRuleSet (rsName : RuleSetName) :
                Lean.CoreM (GlobalRuleSet × Lean.Name × Lean.Name)
                Instances For
                  source
                  def Aesop.Frontend.getGlobalRuleSets (rsNames : Array RuleSetName) :
                  Lean.CoreM (Array (GlobalRuleSet × Lean.Name × Lean.Name))
                  Instances For
                    source
                    def Aesop.Frontend.getDefaultGlobalRuleSets :
                    Lean.CoreM (Array (GlobalRuleSet × Lean.Name × Lean.Name))
                    Instances For
                      source
                      def Aesop.Frontend.getDeclaredGlobalRuleSets :
                      Lean.CoreM (Array (RuleSetName × GlobalRuleSet × Lean.Name × Lean.Name))
                      Instances For
                        source
                        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 α
                        Instances For
                          source
                          def Aesop.Frontend.modifyGlobalRuleSet (rsName : RuleSetName) (f : GlobalRuleSet → GlobalRuleSet) :
                          Lean.CoreM Unit
                          Instances For
                            source
                            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
                            Instances For
                              source
                              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
                              Instances For