Documentation

Lean.Widget.Diff

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.

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
    Instances For

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

      Equations
      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

              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.

              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

                      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