opaque Lean.Widget.showTacticDiff : Lean.Option Bool

def Lean.Widget.ExprDiffTag.toDiffTag (useAfter : Bool) : Lean.Widget.ExprDiffTag → Lean.Widget.DiffTag

Equations

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

def Lean.Widget.ExprDiffTag.toString : Lean.Widget.ExprDiffTag → String

Equations

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

instance Lean.Widget.instToStringExprDiffTag : ToString Lean.Widget.ExprDiffTag

Equations

• Lean.Widget.instToStringExprDiffTag = { toString := Lean.Widget.ExprDiffTag.toString }

structure Lean.Widget.ExprDiff : Type

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 : Lean.SubExpr.PosMap Lean.Widget.ExprDiffTag

  Map from subexpr positions in e₀ to diff points.

• changesAfter : Lean.SubExpr.PosMap Lean.Widget.ExprDiffTag

  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.

instance Lean.Widget.instEmptyCollectionExprDiff : EmptyCollection Lean.Widget.ExprDiff

Equations

• Lean.Widget.instEmptyCollectionExprDiff = { emptyCollection := { changesBefore := ∅, changesAfter := ∅ } }

instance Lean.Widget.instAppendExprDiff : Append Lean.Widget.ExprDiff

Equations

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

instance Lean.Widget.instToStringExprDiff : ToString Lean.Widget.ExprDiff

Equations

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

def Lean.Widget.ExprDiff.insertBeforeChange (p : Lean.SubExpr.Pos) (d : optParam Lean.Widget.ExprDiffTag Lean.Widget.ExprDiffTag.change) (δ : Lean.Widget.ExprDiff) : Lean.Widget.ExprDiff

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

Equations

• Lean.Widget.ExprDiff.insertBeforeChange p d δ = { changesBefore := Lean.RBMap.insert δ.changesBefore p d, changesAfter := δ.changesAfter }

def Lean.Widget.ExprDiff.insertAfterChange (p : Lean.SubExpr.Pos) (d : optParam Lean.Widget.ExprDiffTag Lean.Widget.ExprDiffTag.change) (δ : Lean.Widget.ExprDiff) : Lean.Widget.ExprDiff

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

Equations

• Lean.Widget.ExprDiff.insertAfterChange p d δ = { changesBefore := δ.changesBefore, changesAfter := Lean.RBMap.insert δ.changesAfter p d }

def Lean.Widget.ExprDiff.withChangePos (before : Lean.SubExpr.Pos) (after : Lean.SubExpr.Pos) (d : optParam Lean.Widget.ExprDiffTag Lean.Widget.ExprDiffTag.change) : Lean.Widget.ExprDiff

Equations

• Lean.Widget.ExprDiff.withChangePos before after d = { changesBefore := Lean.RBMap.insert Lean.RBMap.empty before d, changesAfter := Lean.RBMap.insert Lean.RBMap.empty after d }

def Lean.Widget.ExprDiff.withChange (before : Lean.SubExpr) (after : Lean.SubExpr) (d : optParam Lean.Widget.ExprDiffTag Lean.Widget.ExprDiffTag.change) : Lean.Widget.ExprDiff

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

Equations

• Lean.Widget.ExprDiff.withChange before after d = Lean.Widget.ExprDiff.withChangePos before.pos after.pos d

def Lean.Widget.ExprDiff.isEmpty (d : Lean.Widget.ExprDiff) : Bool

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

Equations

• Lean.Widget.ExprDiff.isEmpty d = decide (Lean.RBMap.isEmpty d.changesAfter = true ∧ Lean.RBMap.isEmpty d.changesBefore = true)

partial def Lean.Widget.exprDiffCore (before : Lean.SubExpr) (after : Lean.SubExpr) : Lean.MetaM Lean.Widget.ExprDiff

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.

partial def Lean.Widget.exprDiffCore.piDiff (before : Lean.SubExpr) (after : Lean.SubExpr) : Lean.MetaM Lean.Widget.ExprDiff

def Lean.Widget.exprDiff (e₀ : Lean.Expr) (e₁ : Lean.Expr) (useAfter : optParam Bool true) : Lean.MetaM Lean.Widget.ExprDiff

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.

def Lean.Widget.addDiffTags (useAfter : Bool) (diff : Lean.Widget.ExprDiff) (info₁ : Lean.Widget.CodeWithInfos) : Lean.MetaM Lean.Widget.CodeWithInfos

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.

def Lean.Widget.diffHypothesesBundle (useAfter : Bool) (ctx₀ : Lean.LocalContext) (h₁ : Lean.Widget.InteractiveHypothesisBundle) : Lean.MetaM Lean.Widget.InteractiveHypothesisBundle

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.

def Lean.Widget.diffHypothesesBundle.withTypeDiff (useAfter : Bool) (t₀ : Lean.Expr) (h₁ : Lean.Widget.InteractiveHypothesisBundle) : Lean.MetaM Lean.Widget.InteractiveHypothesisBundle

Equations

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

def Lean.Widget.diffHypotheses (useAfter : Bool) (lctx₀ : Lean.LocalContext) (hs₁ : Array Lean.Widget.InteractiveHypothesisBundle) : Lean.MetaM (Array Lean.Widget.InteractiveHypothesisBundle)

Equations

• Lean.Widget.diffHypotheses useAfter lctx₀ hs₁ = Array.mapM (Lean.Widget.diffHypothesesBundle useAfter lctx₀) hs₁

def Lean.Widget.diffInteractiveGoal (useAfter : Bool) (g₀ : Lean.MVarId) (i₁ : Lean.Widget.InteractiveGoal) : Lean.MetaM Lean.Widget.InteractiveGoal

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.

def Lean.Widget.diffInteractiveGoals (useAfter : Bool) (info : Lean.Elab.TacticInfo) (igs₁ : Lean.Widget.InteractiveGoals) : Lean.MetaM Lean.Widget.InteractiveGoals

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.