How to format your code well

The first time this course ran I did not emphasize good code layout and when I was marking the projects I regretted this. Formatting your code correctly helps a great deal with readability (as I discovered) and so I now look more favourably on people who do this properly. The code I write in the course repository should always conform to the correct standards. Here are the basics.

Indentation

Code in a tactic block gets indented two spaces.

import Mathlib.Tactic

example (a b : ℕ) : a = b → a ^ 2 = b ^ 2 := by -- `by` at the end
  intro h -- proof is indented two spaces in
  rw [h]

If you have a long theorem statement and want to write it over two or more lines then you should indent subsequent lines with four spaces, for example:

import Mathlib.Data.Nat.Basic

theorem le_induction {P : Nat → Prop} {m}
    (h0 : P m) (h1 : ∀ n, m ≤ n → P n → P (n + 1)) :
    ∀ n, m ≤ n → P n := by
  apply Nat.le.rec
  · exact h0
  · exact h1 _

Spaces between operators

a = b, not a=b. See above. Similarly a + b, a ^ b and so on. Also x : T not x:T, and foo := bar not foo:=bar.

Comments

You don’t have to put a comment on every line of code, but please feel free to put comments at points where something is actually happening. Code with comments is easier to read. Just one line -- write explanation here above a tactic is already helpful. For multi-line comments, use /- and -/

Have only one goal

Sometimes you can end up with more than one goal. This can happen for two reasons. Firstly, perhaps you manually created a new goal. For example, perhaps you wrote have intermediate_result : a = b + c := by `` or ``suffices h : a = b + c by. You just created an extra goal on top of the goal which was already there, so the proof should be indented two more spaces.

import Mathlib.Tactic

example (a b c : ℕ) (h : a = b) : a ^ 2 + c = b ^ 2 + c := by
  have h2 : a ^ 2 = b ^ 2 := by -- you made a second goal
    rw [h]
    -- other lines of code would go here, also indented
  rw [h2] -- back to only two space indentation

The other way it can happen is if you use a tactic or apply a function which changes your old goal into more than one goal.

import Mathlib.Tactic

example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q := by
  constructor -- this tactic replaced the goal we were working on with two goals
  · -- so use the right kind of dot (`\.`) and work with one goal at a time
    exact hP
  · exact hQ -- note also extra indentation

Module docstrings

For your projects, you might want to consider writing “module docstrings”, which is a fancy name for “a big comment at the top of each file explaining what happens in the file.” Look at any file in mathlib to see an example, or you can see one here .

Want to know more?

Check out the mathlib library style guidelines on the Lean community pages – not all of it applies to us, but most of the section on tactic mode does.