Documentation

Aesop.Frontend.Saturate

source
def Aesop.Frontend.Parser.usingRuleSets :
Lean.ParserDescr
Instances For
    source
    def Aesop.Frontend.Parser.additionalRule :
    Lean.ParserDescr
    Instances For
      source
      def Aesop.Frontend.Parser.additionalRules :
      Lean.ParserDescr
      Instances For
        source
        def Aesop.ElabM.runForwardElab {α : Type} (goal : Lean.MVarId) (x : ElabM α) :
        Lean.Elab.TermElabM α
        Instances For
          source
          def Aesop.Frontend.mkForwardOptions (maxDepth? : Option Nat) (traceScript : Bool) :
          Lean.CoreM Options'
          Instances For
            source
            def Aesop.Frontend.elabGlobalRuleSets (rsNames : Array Lean.Ident) :
            Lean.CoreM (Array (GlobalRuleSet × Lean.Name × Lean.Name))
            Instances For
              source
              def Aesop.Frontend.elabForwardRule (term : Lean.Term) :
              ElabM LocalRuleSetMember
              Instances For
                source
                def Aesop.Frontend.mkHypForwardRule (fvarId : Lean.FVarId) :
                ElabM LocalRuleSetMember
                Instances For
                  source
                  def Aesop.Frontend.isImplication (e : Lean.Expr) :
                  Lean.MetaM Bool
                  Instances For
                    source
                    def Aesop.Frontend.mkHypImplicationRule? (fvarId : Lean.FVarId) :
                    ElabM (Option LocalRuleSetMember)
                    Instances For
                      source
                      def Aesop.Frontend.addLocalImplications (rs : LocalRuleSet) :
                      ElabM LocalRuleSet
                      Instances For
                        source
                        def Aesop.Frontend.elabAdditionalForwardRules (rs : LocalRuleSet) (rules : Array (Lean.TSyntax `Aesop.Frontend.Parser.additionalRule)) :
                        ElabM LocalRuleSet
                        Instances For
                          source
                          def Aesop.Frontend.elabForwardRuleSetCore (rsNames : Array Lean.Ident) (additionalRules : Array (Lean.TSyntax `Aesop.Frontend.Parser.additionalRule)) (options : Options') :
                          ElabM LocalRuleSet
                          Instances For
                            source
                            def Aesop.Frontend.elabForwardRuleSet (rsNames? : Option (Lean.TSyntax `Aesop.Frontend.Parser.usingRuleSets)) (additionalRules? : Option (Lean.TSyntax `Aesop.Frontend.Parser.additionalRules)) (options : Options') :
                            ElabM LocalRuleSet
                            Instances For
                              source
                              def Aesop.Frontend.evalSaturateCore (stx : Lean.Syntax) (depth? : Option (Lean.TSyntax `num)) (rules? : Option (Lean.TSyntax `Aesop.Frontend.Parser.additionalRules)) (rs? : Option (Lean.TSyntax `Aesop.Frontend.Parser.usingRuleSets)) (traceScript : Bool) :
                              Lean.Elab.Tactic.TacticM Unit
                              Instances For
                                source
                                def Aesop.Frontend.saturate :
                                Lean.ParserDescr
                                Instances For
                                  source
                                  def Aesop.Frontend.saturate? :
                                  Lean.ParserDescr
                                  Instances For
                                    source
                                    def Aesop.Frontend.evalSaturate :
                                    Lean.Elab.Tactic.Tactic
                                    Instances For
                                      source
                                      def Aesop.Frontend.evalSaturate? :
                                      Lean.Elab.Tactic.Tactic
                                      Instances For
                                        source
                                        def Aesop.Frontend.tacticForward____ :
                                        Lean.ParserDescr
                                        Instances For
                                          source
                                          def Aesop.Frontend.tacticForward?____ :
                                          Lean.ParserDescr
                                          Instances For