Don't indent for sections and namespaces.

leanprover / theorem_proving_in_lean

Theorem proving in Lean

Apache License 2.0

47 stars 46 forks source link

Closed Julian closed 3 years ago

Julian commented 3 years ago

Minor style PR in case it's useful.

@fpvandoorn mentioned that in more recent Lean style, their bodies are kept unindented.

This modifies all the examples I see in TPIL to reflect that.

avigad commented 3 years ago

Merged 71f3b11. Thanks!