## Stream: new members

### Topic: Lean formatter

#### Huỳnh Trần Khanh (Feb 11 2021 at 07:01):

in JavaScript there is this pretty tool called prettier that prettifies my code. is there an equivalent tool for Lean? and also is there a Lean linter to catch some style errors?

#### Huỳnh Trần Khanh (Feb 11 2021 at 07:01):

for example i want to ban all uses of theorem in my Lean code because theorem sounds pompous

#### Huỳnh Trần Khanh (Feb 11 2021 at 07:02):

or forbid non terminal simp

#### Johan Commelin (Feb 11 2021 at 07:05):

We don't have a code formatter. There are a bunch of linters in mathlib, but not for non-terminal simp.

#### Johan Commelin (Feb 11 2021 at 07:05):

They do catch unused hypotheses or bad simp lemmas, and things like that

#### Kevin Buzzard (Feb 11 2021 at 08:38):

I don't understand enough about linters to know whether they would be capable of checking for nonterminal simps. Isn't there some sort of limitation as to what they can do? Some nonterminal simps are ok, eg I think simp, ring is ok for closing a goal because even if simpgets smarter it's highly unlikely to break a ring proof which worked before

#### Anne Baanen (Feb 11 2021 at 11:48):

It has been a while so this may have been fixed, but my understanding is that linters can only access the output of a tactic, not the tactic script itself. So finding nonterminal simps is basically undoable (in Lean 3).

#### Anne Baanen (Feb 11 2021 at 11:48):

Writing a Lean formatter in Lean will be difficult too for the same reason.

#### Bryan Gin-ge Chen (Feb 11 2021 at 15:17):

This should be doable in Lean 4, though!

Last updated: May 17 2021 at 21:12 UTC