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

Equations

• Aesop.instInhabitedGoalDiff.default = { oldGoal := default, newGoal := default, addedFVars := default, removedFVars := default, targetChanged := default }

instance Aesop.instInhabitedGoalDiff : Inhabited GoalDiff

Equations

• Aesop.instInhabitedGoalDiff = { default := Aesop.instInhabitedGoalDiff.default }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Aesop.isGoalDiffDefeqTarget oldGoal newGoal = newGoal.withContext do let __do_lift ← oldGoal.getType let __do_lift_1 ← newGoal.getType Aesop.isGoalDiffDefeqExpr __do_lift __do_lift_1

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Diff two goals.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.