Lean.mkMVar vs Lean.Expr.mvar

Stream: lean4

[Eric Wieser]

The former says the latter is the preferred form; should it also be deprecated?

[Kyle Miller]

It probably should, but it's also probably low-priority to deprecate at this moment.

I think the history of mkMVar is that it comes from before Lean had computed fields. It was necessary to use constructors like mkMVar to properly fill in the computed data. Then, computed fields arrived, and using the actual constructor directly was feasible.