Closed nomeata closed 6 months ago
This removes an argument unused since https://github.com/leanprover/lean4/pull/3123
Once leanprover/std4#502 is merged into Std's bump/v4.6.0 branch, we should change this PR to depend on that, and then create a bump/v4.6.0 branch here, and merge this PR into that.
bump/v4.6.0
This removes an argument unused since https://github.com/leanprover/lean4/pull/3123