Documentation

Lean.Widget.Diff

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

A description of the differences between a pair of expressions before, after : Expr. The information can be used to display a 'visual diff' for either before, showing the parts of the expression that are about to change, or after showing which parts of the expression have changed.

• changesBefore :

Map from subexpr positions in e₀ to diff points.

• changesAfter :

A map from subexpr positions in e₁ to 'diff points' which are tags describing how the expression has changed relative to before at the given position.

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

Add a tag at the given position to the changesBefore dict.

Equations
• = { changesBefore := Lean.RBMap.insert δ.changesBefore p d, changesAfter := δ.changesAfter }
Instances For

Add a tag at the given position to the changesAfter dict.

Equations
• = { changesBefore := δ.changesBefore, changesAfter := Lean.RBMap.insert δ.changesAfter p d }
Instances For
Equations
Instances For

Add a tag to the diff at the positions given by before and after.

Equations
Instances For

If true, the expression before and the expression after are identical.

Equations
Instances For
partial def Lean.Widget.exprDiffCore (before : Lean.SubExpr) (after : Lean.SubExpr) :

Computes a diff between before and after expressions.

This works by recursively comparing function arguments.

TODO(ed): experiment with a 'greatest common subexpression' design where given e₀, e₁, find the greatest common subexpressions Xs : Array Expr and a congruence F such that e₀ = F[A₀[..Xs]] and e₀ = F[A₁[..Xs]]. Then, we can have fancy diff highlighting where common subexpressions are not highlighted.

Diffing binders #

Two binding domains are identified if they have the same user name and the same type. The most common tactic that modifies binders is after an intros. To deal with this case, if before = (a : α) → β and after, is not a matching binder (ie: not (a : α) → _) then we instantiate the before variable in a new context and continue diffing β against after.

def Lean.Widget.exprDiff (e₀ : Lean.Expr) (e₁ : Lean.Expr) (useAfter : ) :

Computes the diff for e₀ and e₁. If useAfter is false, e₀, e₁ are interpreted as after, before instead of before, after.

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

Given a diff between before and after : Expr, and the rendered infoAfter : CodeWithInfos for after, this function decorates infoAfter with tags indicating where the expression has changed.

If useAfter == false before and after are swapped.

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

Diffs the given hypothesis bundle against the given local context.

If useAfter == true, ctx₀ is the context before and h₁ is the bundle after. If useAfter == false, these are swapped.

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
def Lean.Widget.diffHypotheses (useAfter : Bool) (lctx₀ : Lean.LocalContext) :
Equations
Instances For

Decorates the given goal i₁ with a diff by comparing with goal g₀. If useAfter is true then i₁ is after and g₀ is before. Otherwise they are swapped.

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

Modifies goalsAfter with additional information about how it is different to goalsBefore. If useAfter is true then igs₁ is the set of interactive goals after the tactic has been applied. Otherwise igs₁ is the set of interactive goals before.

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