Closed kim-em closed 1 year ago
The intent here is to free up Lean to be able to change the instance naming algorithm, possibly even making them inaccessible, per https://github.com/leanprover/lean4/issues/2343.
The intent here is to free up Lean to be able to change the instance naming algorithm, possibly even making them inaccessible, per https://github.com/leanprover/lean4/issues/2343.