An action in an edit script to transform one source sequence into a target sequence.

- insert: Lean.Diff.Action
Insert the item into the source

- delete: Lean.Diff.Action
Delete the item from the source

- skip: Lean.Diff.Action
Leave the item in the source

## Instances For

## Equations

- Lean.Diff.instReprAction = { reprPrec := Lean.Diff.reprAction✝ }

## Equations

- Lean.Diff.instBEqAction = { beq := Lean.Diff.beqAction✝ }

## Equations

- Lean.Diff.instHashableAction = { hash := Lean.Diff.hashAction✝ }

## Equations

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

Determines a prefix to show on a given line when printing diff results.

For `delete`

, the prefix is `"-"`

, for `insert`

, it is `"+"`

, and for `skip`

it is `" "`

.

## Equations

- Lean.Diff.Action.delete.linePrefix = "-"
- Lean.Diff.Action.insert.linePrefix = "+"
- Lean.Diff.Action.skip.linePrefix = " "

## Instances For

A histogram entry consists of the number of times the element occurs in the left and right input arrays along with an index at which the element can be found, if applicable.

- leftCount : Nat
How many times the element occurs in the left array

An index of the element in the left array, if applicable

Invariant: the count is non-zero iff there is a saved index

- rightCount : Nat
How many times the element occurs in the right array

An index of the element in the right array, if applicable

Invariant: the count is non-zero iff there is a saved index

## Instances For

Invariant: the count is non-zero iff there is a saved index

Invariant: the count is non-zero iff there is a saved index

A histogram for arrays maps each element to a count and, if applicable, an index.

## Equations

- Lean.Diff.Histogram α lsize rsize = Std.HashMap α (Lean.Diff.Histogram.Entry α lsize rsize)

## Instances For

Add an element from the left array to a histogram

## Equations

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

## Instances For

Add an element from the right array to a histogram

## Equations

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

## Instances For

Given two `Subarray`

s, find their common prefix and return their differing suffixes

## Equations

- Lean.Diff.matchPrefix left right = Lean.Diff.matchPrefix.go left right #[]

## Instances For

Given two `Subarray`

s, find their common suffix and return their differing prefixes

## Equations

- Lean.Diff.matchSuffix left right = Lean.Diff.matchSuffix.go left right 0

## Instances For

Finds the least common subsequence of two arrays using a variant of jgit's histogram diff algorithm.

Unlike jgit's implementation, this one does not perform a cutoff on histogram bucket sizes, nor does it fall back to the Myers diff algorithm. This means that it has quadratic worst-case complexity. Empirically, however, even quadratic cases of this implementation can handle hundreds of megabytes in a second or so, and it is intended to be used for short strings like error messages. Be cautious when applying it to larger workloads.

Shows a line-by-line edit script with markers for added and removed lines.

## Equations

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