source
@[reducible, inline]
abbrev Lean.Perm :
Type
Equations

- Lean.Perm = Std.HashMap Nat Nat

Instances For

source
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.

Instances For