@[reducible, inline]

abbrev Lean.Perm : Type

Equations

• Lean.Perm = Std.HashMap Nat Nat

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.

Equations

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