make binder types explicit

Author: fpvandoorn

templates/contribute/style.md

@@ -181,6 +181,11 @@ theorem mem_split {x : T} {l : List T} : x ∈ l → ∃ s t : List T, l = s ++
           have H4 : y  ::  l = (y :: s) ++ (x :: t) := by rw [H3]; rfl
           Exists.intro (y :: s) (Exists.intro t H4)))
 ```
+The type of all arguments of a declaration should be given,
+even if Lean can figure out this type information by itself.
+This makes it easier to understand the definition when seeing it on a webpage like GitHub.
+For the same reason, the return type of all declarations should also be given
+(Lean enforces this only for theorems).
 
 A short declaration can be written on a single line:
 ```lean
@@ -325,9 +330,10 @@ lemma zero_le : ∀ n : ℕ, 0 ≤ n
 
 ### Binders
 
-Use a space after binders:
+Use a space after binders. Also, the binder type should generally be written explicitly,
+even if Lean doesn't need this information.
 ```lean
-example : ∀ α : Type, ∀ x : α, ∃ y, y = x :=
+example : ∀ α : Type, ∀ x : α, ∃ y : α, y = x :=
   fun (α : Type) (x : α) ↦ Exists.intro x rfl
 ```
 
@@ -528,7 +534,7 @@ can be accessed by commenting `!bench` on a PR.
 
 Authors should assure that their contributions do not cause significant
 performance regressions. In particular, if the PR touches significant components
-of the language like adding instances, adding `simp` lemmas, changing imports,
+of the language like adding new classes, instances, or `simp` lemmas, changing imports,
 or creating new definitions, then authors should benchmark their changes
 proactively.