Closed Vtec234 closed 2 years ago
Mostly adapting to leanprover/lean4#1291.
Merging as it's hopefully uncontroversial.
Mostly adapting to leanprover/lean4#1291.