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 will be looking more favourably on people who do this properly this year. 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.
example (a b : ℕ) : a = b → a ^ 2 = b ^ 2 :=
begin
intro h, -- I am two spaces in, not under `begin`
rw h,
end
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.
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, or suffices : a = b + c,. You just created an extra goal on top of the goal which was already there, so this one extra goal needs to go in brackets and get indented two more spaces.
example (a b c : ℕ) (h : a = b) : a ^ 2 + c = b ^ 2 + c :=
begin
have h2 : a ^ 2 = b ^ 2, -- you made a second goal
{ rw h,
-- other lines of code would go here, also indented
},
rw h2, -- back to only two space indentation
end
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.
example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q :=
begin
split, -- this tactic replaced the goal we were working on with two goals
{ -- so they both need to go in curly brackets
exact hP, },
{ exact hQ, },
end
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.
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.