search

leanprover-community / batteries

The "batteries included" extended library for the Lean programming language and theorem prover
Apache License 2.0
242 stars 101 forks source link

chore: fix more Std -> Batteries #887

Closed digama0 closed 3 weeks ago

digama0 commented 2 months ago

It was still present in the namespaces Std.Tactic.Lint and Std.CodeAction.

mattrobball commented 3 weeks ago

@fgdorais do you want do the honors since I touched the code?

grunweg commented 3 weeks ago

Thanks for merging this PR!

grunweg commented 3 weeks ago

Thanks for merging this PR!