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 `GoalDiff`

s 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.

For a goal diff between an old goal with local context `Γ`

and a new goal with
local context `Δ`

, we expect that

```
Δ = (Γ \ removedFVars) ∪ addedFVars
```

when the local contexts are viewed as sets of `FVarId`

s (excluding
implementation detail hypotheses).

As an optimisation, the goal diff additionally contains an `fvarSubst : FVarIdSubst`

which tracks renamings of hypotheses. When the substitution
contains a mapping `h ↦ h'`

, this means that `h`

was renamed to `h'`

. Note that
we do not guarantee that for all such mappings, `h`

actually appears in the old
goal and `h'`

in the new goal. But if they do, `fvarSubst(T)`

and `T'`

must be
defeq in the context of the new goal, where `h : T`

, `h' : T'`

and
`fvarSubst(T)`

is the application of the substitution to `T`

. If `h`

and `h'`

are `let`

decls with values `v`

and `v'`

, `fvarSubst(v)`

must additionally be
defeq to `v'`

.

The `fvarSubst`

is semantically irrelevant: it does not influence the sets of
added and removed hypotheses. However, it is an important performance
optimisation, so rules should strive to generate accurate substitutions whenever
possible.

- addedFVars : Std.HashSet Lean.FVarId
`FVarId`

s that appear in the new goal, but not in the old goal. - removedFVars : Std.HashSet Lean.FVarId
`FVarId`

s that appear in the old goal, but not in the new goal. - fvarSubst : Aesop.FVarIdSubst
An

`FVarId`

substitution that tracks hypotheses which have been renamed (but have not otherwise been modified).

## Instances For

## Equations

- Aesop.instInhabitedGoalDiff = { default := { addedFVars := default, removedFVars := default, fvarSubst := default } }

## Equations

- Aesop.GoalDiff.empty = { addedFVars := ∅, removedFVars := ∅, fvarSubst := ∅ }

## Instances For

## Equations

- Aesop.instEmptyCollectionGoalDiff = { emptyCollection := Aesop.GoalDiff.empty }

## Equations

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

## Instances For

Diff two goals.

## Equations

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

## Instances For

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₃`

.

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

- One or more equations did not get rendered due to their size.
- Aesop.GoalDiff.checkCore.isDefeqLocalDecl x✝ x = pure false

## Instances For

## Equations

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