Documentation

Aesop.BuiltinRules.Subst

source
def Aesop.BuiltinRules.matchSubstitutableIff? (e : Lean.Expr) :
Option (Lean.Expr × Lean.Expr)
Equations
    Instances For
      source
      def Aesop.BuiltinRules.prepareIff? (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) :
      ScriptM (Option (Lean.MVarId × Lean.FVarId))
      Equations
        Instances For
          source
          def Aesop.BuiltinRules.prepareIffs (mvarId : Lean.MVarId) (fvarIds : Array Lean.FVarId) :
          ScriptM (Lean.MVarId × Array Lean.FVarId)
          Equations
            Instances For
              source
              def Aesop.BuiltinRules.substEqs? (goal : Lean.MVarId) (fvarIds : Array Lean.FVarId) :
              ScriptM (Option Lean.MVarId)
              Equations
                Instances For
                  source
                  def Aesop.BuiltinRules.substEqsAndIffs? (goal : Lean.MVarId) (fvarIds : Array Lean.FVarId) :
                  ScriptM (Option Lean.MVarId)
                  Equations
                    Instances For
                      source
                      def Aesop.BuiltinRules.subst :
                      RuleTac
                      Equations
                        Instances For