structure Aesop.GoalDiff : Type

A representation of the differences between two goals. Each Aesop rule produces a GoalDiff between the goal on which the rule was run (the 'old goal') and each of the subgoals produced by the rule (the 'new goals').

We use the produced GoalDiffs to update stateful data structures which cache information about Aesop goals and for which it is more efficient to update the cached information than to recompute it for each goal.

Hypotheses are identified by their FVarId and the RPINF of their type and value (if any). This means that when a hypothesis h : T with FVarId i appears in the old goal and h : T' with FVarId i appears in the new goal, but the RPINF of T is not equal to the RPINF of T', then h is treated as both added (with the new type) and removed (with the old type). This can happen when the type of a hyp changes to another type that is definitionally equal at default, but not at reducible transparency.

The target is identified by RPINF.

• oldGoal : Lean.MVarId

  The old goal.

• newGoal : Lean.MVarId

  The new goal.

• addedFVars : Std.HashSet Lean.FVarId

  FVarIds that appear in the new goal, but not (or with a different type) in the old goal.

• removedFVars : Std.HashSet Lean.FVarId

  FVarIds that appear in the old goal, but not (or with a different type) in the new goal.

• targetChanged : Lean.LBool

  Is the old goal's target RPINF equal to the new goal's target RPINF?

instance Aesop.instInhabitedGoalDiff : Inhabited GoalDiff

def Aesop.GoalDiff.empty (oldGoal newGoal : Lean.MVarId) : GoalDiff

def Aesop.isRPINFEqual (goal₁ goal₂ : Lean.MVarId) (e₁ e₂ : Lean.Expr) : BaseM Bool

def Aesop.isRPINFEqualLDecl (goal₁ goal₂ : Lean.MVarId) (ldecl₁ ldecl₂ : Lean.LocalDecl) : BaseM Bool

def Aesop.getNewFVars (oldGoal newGoal : Lean.MVarId) (oldLCtx newLCtx : Lean.LocalContext) : BaseM (Std.HashSet Lean.FVarId)

def Aesop.diffGoals (old new : Lean.MVarId) : BaseM GoalDiff

Diff two goals.

def Aesop.GoalDiff.targetChanged' (diff : GoalDiff) : BaseM Bool

def Aesop.GoalDiff.comp (diff₁ diff₂ : GoalDiff) : GoalDiff

If diff₁ is the difference between goals g₁ and g₂ and diff₂ is the difference between g₂ and g₃, then diff₁.comp diff₂ is the difference between g₁ and g₃.

We assume that a hypothesis whose RPINF changed between g₁ and g₂ does not change back, i.e. the hypothesis' RPINF is still different between g₁ and g₃.

def Aesop.GoalDiff.checkCore (diff : GoalDiff) (old new : Lean.MVarId) : BaseM (Option Lean.MessageData)

def Aesop.GoalDiff.check (diff : GoalDiff) (old new : Lean.MVarId) : BaseM (Option Lean.MessageData)