@[reducible, inline]

abbrev Lean.Perm : Type

def Lean.sortExprs (es : Array Expr) (lt : Bool := true) : Array Expr × Perm

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.