Documentation

Aesop.Forward.State.ApplyGoalDiff

source
def Aesop.ForwardState.applyGoalDiff (rs : LocalRuleSet) (diff : GoalDiff) (fs : ForwardState) :
BaseM (ForwardState × Array ForwardRuleMatch)

Apply a goal diff to the state, adding and removing hypotheses as indicated by the diff.

Equations
    Instances For
      source
      def Aesop.ForwardState.applyGoalDiff.eraseHyp (h : Lean.FVarId) (fs : ForwardState) :
      BaseM ForwardState
      Equations
        Instances For
          source
          def Aesop.ForwardState.applyGoalDiff.addHyp (rs : LocalRuleSet) (diff : GoalDiff) (h : Lean.FVarId) (fs : ForwardState) (ruleMatches : Array ForwardRuleMatch) :
          BaseM (ForwardState × Array ForwardRuleMatch)
          Equations
            Instances For
              source
              def Aesop.ForwardState.applyGoalDiff.updateTarget (rs : LocalRuleSet) (diff : GoalDiff) (fs : ForwardState) (ruleMatches : Array ForwardRuleMatch) :
              BaseM (ForwardState × Array ForwardRuleMatch)
              Equations
                Instances For
                  source
                  def Aesop.ForwardState.applyGoalDiff.updateHypTypes (diff : GoalDiff) (hypTypes : Lean.PHashSet RPINF) :
                  BaseM (Lean.PHashSet RPINF)
                  Equations
                    Instances For