perf: skip `preprocessOutParam` for noMVars queries This reverts part of the `OrderDual` workaround from #12286. The `preprocessOutParam` step is morally not needed when the type has no metavariables, because output params should be uniquely determined by the input params. The optimization was removed because semireducible type aliases like `OrderDual` caused TC resolution to fail (e.g. `FunLike F (OrderDual α) (OrderDual β)` where the last two arguments are output parameters — without `preprocessOutParam`, TC resolution fails because it cannot unfold `OrderDual`). This is an experimental branch for testing whether Mathlib's `OrderDual` refactoring has progressed enough to restore this optimization.
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.