Documentation

Aesop.Frontend.Extension

source
def Aesop.Frontend.extensionDescr (rsName : RuleSetName) :
Lean.SimpleScopedEnvExtension.Descr BaseRuleSetMember BaseRuleSet
Equations
    Instances For
      source
      def Aesop.Frontend.declareRuleSetUnchecked (rsName : RuleSetName) (isDefault : Bool) :
      IO Unit
      Equations
        Instances For
          source
          def Aesop.Frontend.isRuleSetDeclared (rsName : RuleSetName) :
          IO Bool
          Equations
            Instances For
              source
              def Aesop.Frontend.checkRuleSetNotDeclared {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT IO m] (rsName : RuleSetName) :
              m Unit
              Equations
                Instances For
                  source
                  def Aesop.Frontend.declareRuleSet {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT IO m] (rsName : RuleSetName) (isDefault : Bool) :
                  m Unit
                  Equations
                    Instances For
                      source
                      def Aesop.Frontend.getGlobalRuleSetData {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT IO m] (rsName : RuleSetName) :
                      m (RuleSetExtension × Lean.Name × Lean.Meta.SimpExtension × Lean.Name × Lean.Meta.Simp.SimprocExtension)
                      Equations
                        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
                          Equations
                            Instances For
                              source
                              def Aesop.Frontend.getGlobalRuleSet (rsName : RuleSetName) :
                              Lean.CoreM (GlobalRuleSet × Lean.Name × Lean.Name)
                              Equations
                                Instances For
                                  source
                                  def Aesop.Frontend.getGlobalRuleSets (rsNames : Array RuleSetName) :
                                  Lean.CoreM (Array (GlobalRuleSet × Lean.Name × Lean.Name))
                                  Equations
                                    Instances For
                                      source
                                      def Aesop.Frontend.getDefaultGlobalRuleSets :
                                      Lean.CoreM (Array (GlobalRuleSet × Lean.Name × Lean.Name))
                                      Equations
                                        Instances For
                                          source
                                          def Aesop.Frontend.getDeclaredGlobalRuleSets :
                                          Lean.CoreM (Array (RuleSetName × GlobalRuleSet × Lean.Name × Lean.Name))
                                          Equations
                                            Instances For
                                              source
                                              def Aesop.Frontend.modifyGetGlobalRuleSet {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT IO m] [Lean.MonadEnv m] {α : Type} (rsName : RuleSetName) (f : GlobalRuleSet → α × GlobalRuleSet) :
                                              m α
                                              Equations
                                                Instances For
                                                  source
                                                  def Aesop.Frontend.modifyGlobalRuleSet (rsName : RuleSetName) (f : GlobalRuleSet → GlobalRuleSet) :
                                                  Lean.CoreM Unit
                                                  Equations
                                                    Instances For
                                                      source
                                                      def Aesop.Frontend.addGlobalRule {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT IO m] [Lean.MonadEnv m] [Lean.MonadResolveName m] (rsName : RuleSetName) (r : GlobalRuleSetMember) (kind : Lean.AttributeKind) (checkNotExists : Bool) :
                                                      m Unit
                                                      Equations
                                                        Instances For
                                                          source
                                                          def Aesop.Frontend.eraseGlobalRules {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT IO m] [Lean.MonadEnv m] (rsf : RuleSetNameFilter) (rf : RuleFilter) (checkExists : Bool) :
                                                          m Unit
                                                          Equations
                                                            Instances For
                                                              source
                                                              def Aesop.Frontend.eraseGlobalRules.go {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT IO m] [Lean.MonadEnv m] (rf : RuleFilter) (anyErased : Bool) (rsName : RuleSetName) :
                                                              m Bool
                                                              Equations
                                                                Instances For