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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Aesop.ForwardState.applyGoalDiff.eraseHyp (h : Lean.FVarId) (fs : ForwardState) :
    BaseM ForwardState
    Equations
    • One or more equations did not get rendered due to their size.
    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
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Aesop.ForwardState.applyGoalDiff.updateTarget (rs : LocalRuleSet) (diff : GoalDiff) (fs : ForwardState) (ruleMatches : Array ForwardRuleMatch) :
        BaseM (ForwardState × Array ForwardRuleMatch)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Aesop.ForwardState.applyGoalDiff.updateHypTypes (diff : GoalDiff) (hypTypes : Lean.PHashSet RPINF) :
          BaseM (Lean.PHashSet RPINF)
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For