Documentation

Aesop.RuleTac.Apply

source
def Aesop.RuleTac.applyExpr' (goal : Lean.MVarId) (e : Lean.Expr) (eStx : Lean.Term) (patSubst? : Option Substitution) (md : Lean.Meta.TransparencyMode) :
BaseM RuleApplication
Instances For
    source
    def Aesop.RuleTac.applyExpr (goal : Lean.MVarId) (e : Lean.Expr) (eStx : Lean.Term) (patSubsts? : Option (Array Substitution)) (md : Lean.Meta.TransparencyMode) :
    BaseM RuleTacOutput
    Instances For
      source
      def Aesop.RuleTac.applyConst (decl : Lean.Name) (md : Lean.Meta.TransparencyMode) :
      RuleTac
      Instances For
        source
        def Aesop.RuleTac.applyTerm (stx : Lean.Term) (md : Lean.Meta.TransparencyMode) :
        RuleTac
        Instances For
          source
          def Aesop.RuleTac.apply (t : RuleTerm) (md : Lean.Meta.TransparencyMode) :
          RuleTac
          Instances For
            source
            def Aesop.RuleTac.applyConsts (decls : Array Lean.Name) (md : Lean.Meta.TransparencyMode) :
            RuleTac
            Instances For