Documentation

Lean.Util.SortExprs

@[reducible, inline]
abbrev Lean.Perm :
Equations
    Instances For

      Sorts the given expressions using Expr.lt, and creates a "permutation map" storing the new position of each expression. If lt := false, then sorts expressions in decreasing order.

      Equations
        Instances For