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.

def Aesop.ForwardState.applyGoalDiff.eraseHyp (h : Lean.FVarId) (fs : ForwardState) : BaseM ForwardState

Equations

• Aesop.ForwardState.applyGoalDiff.eraseHyp h fs = do let __do_lift ← liftM h.getType let __do_lift ← Aesop.rpinf __do_lift pure (Aesop.ForwardState.eraseHyp h __do_lift fs)

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.

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.

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.