Lean4 code formatter
Production-worthy formatter for lean4. Right now it copes with important open source libraries on the model of clang-format's configuration, which is a real trick given the partial elaboration you need (with backtracking). But that works. mathlib4 is the final boss, I don't currently even have a plan without per-directory quirks files which is probably a nonstarter.