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 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 T is not defeq to 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 up to defeq. All defeq comparisons are made at reducible transparency and metavariables are treated as rigid.

• 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 : Bool

  Is the old goal's target defeq to the new goal's target?

def Aesop.instInhabitedGoalDiff.default : GoalDiff

instance Aesop.instInhabitedGoalDiff : Inhabited GoalDiff

def Aesop.isGoalDiffDefeqExpr (oldExpr newExpr : Lean.Expr) : Lean.MetaM Bool

def Aesop.isGoalDiffDefeqTarget (oldGoal newGoal : Lean.MVarId) : Lean.MetaM Bool

def Aesop.isGoalDiffDefeqLDecl (oldLDecl newLDecl : Lean.LocalDecl) : Lean.MetaM Bool

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

def Aesop.diffGoals (oldGoal newGoal : Lean.MVarId) : BaseM GoalDiff

Diff two goals.

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 which changed between g₁ and g₂ does not change back, i.e. the hypothesis is still different between g₁ and g₃, and similar for the targets.

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)