Documentation

Aesop.Builder.Tactic

source
def Aesop.matchByTactic? :
Lean.Term → Option (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)
Equations
    Instances For
      source
      def Aesop.RuleBuilder.tacticIMode (imode? : Option IndexingMode) :
      IndexingMode
      Equations
        Instances For
          source
          def Aesop.RuleBuilder.tacticCore (t : Lean.Name ⊕ Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) (imode? : Option IndexingMode) (phase : PhaseSpec) :
          Lean.MetaM LocalRuleSetMember
          Equations
            Instances For
              source
              def Aesop.RuleBuilder.tactic :
              RuleBuilder
              Equations
                Instances For