HepLean Documentation

Aesop.Builder.Tactic

source
def Aesop.matchByTactic? :
Lean.Term → Option (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Aesop.RuleBuilder.tacticIMode (imode? : Option Aesop.IndexingMode) :
    Aesop.IndexingMode
    Equations
    Instances For
      source
      def Aesop.RuleBuilder.tacticCore (t : Lean.Name ⊕ Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) (imode? : Option Aesop.IndexingMode) (phase : Aesop.PhaseSpec) :
      Lean.MetaM Aesop.LocalRuleSetMember
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Aesop.RuleBuilder.tactic :
        Aesop.RuleBuilder
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For