docs(tactics): add docstrings to various tactics (#1)

library/data/buffer/parser.lean

@@ -9,6 +9,7 @@ inductive parse_result (α : Type)
 | done (pos : ℕ) (result : α) : parse_result
 | fail (pos : ℕ) (expected : dlist string) : parse_result
 
+/-- The parser monad. If you are familiar with the Parsec library in Haskell, you will understand this.  -/
 def parser (α : Type) :=
 ∀ (input : char_buffer) (start : ℕ), parse_result α
 
@@ -171,6 +172,7 @@ many p >> eps
 def many1 (p : parser α) : parser (list α) :=
 list.cons <$> p <*> many p
 
+/-- Matches one of more occurences of the char parser `p` and implodes them into a string. -/
 def many_char1 (p : parser char) : parser string :=
 list.as_string <$> many1 p
 

library/init/algebra/order.lean

@@ -15,15 +15,18 @@ universe u
 variables {α : Type u}
 
 set_option auto_param.check_exists false
+/-- A preorder is a reflexive, transitive relation `≤` with `a < b` defined in the obvious way. -/
 class preorder (α : Type u) extends has_le α, has_lt α :=
 (le_refl : ∀ a : α, a ≤ a)
 (le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
 (lt := λ a b, a ≤ b ∧ ¬ b ≤ a)
 (lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) . order_laws_tac)
 
+/-- A partial order is a reflexive, transitive, antisymmetric relation `≤`. -/
 class partial_order (α : Type u) extends preorder α :=
 (le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b)
 
+/-- A linear order is reflexive, transitive, antisymmetric and total relation `≤`.-/
 class linear_order (α : Type u) extends partial_order α :=
 (le_total : ∀ a b : α, a ≤ b ∨ b ≤ a)
 

library/init/category/alternative.lean

@@ -20,7 +20,7 @@ variables {f : Type u → Type v} [alternative f] {α : Type u}
 
 @[inline] def failure : f α :=
 alternative.failure f
-
+/-- If the condition `p` is decided to be false, then fail, otherwise, return unit. -/
 @[inline] def guard {f : Type → Type v} [alternative f] (p : Prop) [decidable p] : f unit :=
 if p then pure () else failure
 

library/init/coe.lean

@@ -27,6 +27,7 @@ prelude
 import init.data.list.basic init.data.subtype.basic init.data.prod
 universes u v
 
+/-- Can perform a lifting operation `↑a`. -/
 class has_lift (a : Sort u) (b : Sort v) :=
 (lift : a → b)
 

library/init/core.lean

@@ -10,29 +10,32 @@ prelude
 notation `Prop` := Sort 0
 notation f ` $ `:1 a:0 := f a
 
-/- Logical operations and relations -/
+/- Reserving notation. We do this sot that the precedence of all of the operators
+can be seen in one place and to prevent core notation being accidentally overloaded later.  -/
+
+/- Notation for logical operations and relations -/
 
 reserve prefix `¬`:40
-reserve prefix `~`:40
+reserve prefix `~`:40    -- not used
 reserve infixr ` ∧ `:35
 reserve infixr ` /\ `:35
 reserve infixr ` \/ `:30
 reserve infixr ` ∨ `:30
 reserve infix ` <-> `:20
 reserve infix ` ↔ `:20
-reserve infix ` = `:50
-reserve infix ` == `:50
+reserve infix ` = `:50   -- eq
+reserve infix ` == `:50  -- heq
 reserve infix ` ≠ `:50
-reserve infix ` ≈ `:50
-reserve infix ` ~ `:50
-reserve infix ` ≡ `:50
-reserve infixl ` ⬝ `:75
-reserve infixr ` ▸ `:75
-reserve infixr ` ▹ `:75
+reserve infix ` ≈ `:50   -- has_equiv.equiv
+reserve infix ` ~ `:50   -- used as local notation for relations
+reserve infix ` ≡ `:50   -- not used
+reserve infixl ` ⬝ `:75  -- not used
+reserve infixr ` ▸ `:75  -- eq.subst
+reserve infixr ` ▹ `:75  -- not used
 
 /- types and type constructors -/
 
-reserve infixr ` ⊕ `:30
+reserve infixr ` ⊕ `:30  -- sum (defined in init/data/sum/basic.lean)
 reserve infixr ` × `:35
 
 /- arithmetic operations -/
@@ -45,7 +48,7 @@ reserve infixl ` % `:70
 reserve prefix `-`:100
 reserve infixr ` ^ `:80
 
-reserve infixr ` ∘ `:90                 -- input with \comp
+reserve infixr ` ∘ `:90  -- function composition
 
 reserve infix ` <= `:50
 reserve infix ` ≤ `:50
@@ -69,18 +72,18 @@ reserve infix ` ⊆ `:50
 reserve infix ` ⊇ `:50
 reserve infix ` ⊂ `:50
 reserve infix ` ⊃ `:50
-reserve infix ` \ `:70
+reserve infix ` \ `:70   -- symmetric difference
 
 /- other symbols -/
 
-reserve infix ` ∣ `:50
-reserve infixl ` ++ `:65
-reserve infixr ` :: `:67
-reserve infixl `; `:1
+reserve infix ` ∣ `:50   -- has_dvd.dvd. Note this is different to `|`.
+reserve infixl ` ++ `:65 -- has_append.append
+reserve infixr ` :: `:67 -- list.cons
+reserve infixl `; `:1    -- has_andthen.andthen
 
 universes u v w
 
-/-
+/--
 The kernel definitional equality test (t =?= s) has special support for id_delta applications.
 It implements the following rules
 
@@ -157,9 +160,18 @@ constant quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α
 
 constant quot.ind {α : Sort u} {r : α → α → Prop} {β : quot r → Prop} :
   (∀ a : α, β (quot.mk r a)) → ∀ q : quot r, β q
+
+Also the reduction rule:
+
+quot.lift f _ (quot.mk a) ~~> f a
+
 -/
 init_quotient
 
+/-- Heterogeneous equality.
+It's purpose is to write down equalities between terms whose types are not definitionally equal.
+For example, given `x : vector α n` and `y : vector α (0+n)`, `x = y` doesn't typecheck but `x == y` does.
+ -/
 inductive heq {α : Sort u} (a : α) : Π {β : Sort u}, β → Prop
 | refl : heq a
 
@@ -389,7 +401,7 @@ attribute [pattern] has_zero.zero has_one.one bit0 bit1 has_add.add has_neg.neg
 def insert {α : Type u} {γ : Type v} [has_insert α γ] : α → γ → γ :=
 has_insert.insert
 
-/- The empty collection -/
+/-- The singleton collection -/
 def singleton {α : Type u} {γ : Type v} [has_emptyc γ] [has_insert α γ] (a : α) : γ :=
 has_insert.insert a ∅
 

library/init/data/array/basic.lean

@@ -7,21 +7,22 @@ prelude
 import init.data.nat init.data.bool init.ite_simp
 universes u v w
 
-/- In the VM, d_array is implemented a persistent array. -/
+/-- In the VM, d_array is implemented as a persistent array. -/
 structure d_array (n : nat) (α : fin n → Type u) :=
 (data : Π i : fin n, α i)
 
 namespace d_array
 variables {n : nat} {α : fin n → Type u} {β : Type v}
 
+/-- The empty array. -/
 def nil {α} : d_array 0 α :=
 {data := λ ⟨x, h⟩, absurd h (nat.not_lt_zero x)}
 
-/- has builtin VM implementation -/
+/-- `read a i` reads the `i`th member of `a`. Has builtin VM implementation. -/
 def read (a : d_array n α) (i : fin n) : α i :=
 a.data i
 
-/- has builtin VM implementation -/
+/-- `write a i v` sets the `i`th member of `a` to be `v`. Has builtin VM implementation. -/
 def write (a : d_array n α) (i : fin n) (v : α i) : d_array n α :=
 {data := λ j, if h : i = j then eq.rec_on h v else a.read j}
 
@@ -31,11 +32,11 @@ def iterate_aux (a : d_array n α) (f : Π i : fin n, α i → β → β) : Π (
   let i : fin n := ⟨j, h⟩ in
   f i (a.read i) (iterate_aux j (le_of_lt h) b)
 
-/- has builtin VM implementation -/
+/-- Fold over the elements of the given array in ascending order. Has builtin VM implementation. -/
 def iterate (a : d_array n α) (b : β) (f : Π i : fin n, α i → β → β) : β :=
 iterate_aux a f n (le_refl _) b
 
-/- has builtin VM implementation -/
+/-- Map the array. Has builtin VM implementation. -/
 def foreach (a : d_array n α) (f : Π i : fin n, α i → α i) : d_array n α :=
 iterate a a $ λ i v a', a'.write i (f i v)
 
@@ -73,6 +74,7 @@ protected def beq_aux [∀ i, decidable_eq (α i)] (a b : d_array n α) : Π (i
 | 0     h := tt
 | (i+1) h := if a.read ⟨i, h⟩ = b.read ⟨i, h⟩ then beq_aux i (le_of_lt h) else ff
 
+/-- Boolean element-wise equality check. -/
 protected def beq [∀ i, decidable_eq (α i)] (a b : d_array n α) : bool :=
 d_array.beq_aux a b n (le_refl _)
 
@@ -131,10 +133,11 @@ instance [∀ i, decidable_eq (α i)] : decidable_eq (d_array n α) :=
 
 end d_array
 
+/-- A non-dependent array (see `d_array`). Implemented in the VM as a persistent array.  -/
 def array (n : nat) (α : Type u) : Type u :=
 d_array n (λ _, α)
 
-/- has builtin VM implementation -/
+/-- `mk_array n v` creates a new array of length `n` where each element is `v`. Has builtin VM implementation. -/
 def mk_array {α} (n) (v : α) : array n α :=
 {data := λ _, v}
 
@@ -150,9 +153,11 @@ d_array.read a i
 def write (a : array n α) (i : fin n) (v : α) : array n α :=
 d_array.write a i v
 
+/-- Fold array starting from 0, folder function includes an index argument. -/
 def iterate (a : array n α) (b : β) (f : fin n → α → β → β) : β :=
 d_array.iterate a b f
 
+/-- Map each element of the given array with an index argument. -/
 def foreach (a : array n α) (f : fin n → α → α) : array n α :=
 iterate a a (λ i v a', a'.write i (f i v))
 
@@ -180,14 +185,14 @@ a.rev_foldl [] (::)
 lemma push_back_idx {j n} (h₁ : j < n + 1) (h₂ : j ≠ n) : j < n :=
 nat.lt_of_le_and_ne (nat.le_of_lt_succ h₁) h₂
 
-/- has builtin VM implementation -/
+/-- `push_back a v` pushes value `v` to the end of the array. Has builtin VM implementation. -/
 def push_back (a : array n α) (v : α) : array (n+1) α :=
 {data := λ ⟨j, h₁⟩, if h₂ : j = n then v else a.read ⟨j, push_back_idx h₁ h₂⟩}
 
 lemma pop_back_idx {j n} (h : j < n) : j < n + 1 :=
 nat.lt.step h
 
-/- has builtin VM implementation -/
+/-- Discard _last_ element in the array. Has builtin VM implementation. -/
 def pop_back (a : array (n+1) α) : array n α :=
 {data := λ ⟨j, h⟩, a.read ⟨j, pop_back_idx h⟩}
 

library/init/data/repr.lean

@@ -10,9 +10,27 @@ open sum subtype nat
 
 universes u v
 
+/-- 
+Implement `has_repr` if the output string is valid lean code that evaluates back to the original object.
+If you just want to view the object as a string for a trace message, use `has_to_string`.
+
+### Example:
+
+```
+#eval to_string "hello world"
+-- [Lean] "hello world"
+#eval repr "hello world" 
+-- [Lean] "\"hello world\""
+```
+
+Reference: https://github.com/leanprover/lean/issues/1664
+
+ -/
 class has_repr (α : Type u) :=
 (repr : α → string)
 
+/-- `repr` is similar to `to_string` except that we should have the property `eval (repr x) = x` for most sensible datatypes. 
+Hence, `repr "hello"` has the value `"\"hello\""` not `"hello"`.  -/
 def repr {α : Type u} [has_repr α] : α → string :=
 has_repr.repr
 

library/init/data/to_string.lean

@@ -11,6 +11,11 @@ open sum subtype nat
 
 universes u v
 
+/-- Convert the object into a string for tracing/display purposes. 
+Similar to Haskell's `show`.
+See also `has_repr`, which is used to output a string which is a valid lean code.
+See also `has_to_format` and `has_to_tactic_format`, `format` has additional support for colours and pretty printing multilines.
+ -/
 class has_to_string (α : Type u) :=
 (to_string : α → string)
 

library/init/function.lean

@@ -77,12 +77,12 @@ def bijective (f : α → β) := injective f ∧ surjective f
 lemma bijective_comp {g : β → φ} {f : α → β} : bijective g → bijective f → bijective (g ∘ f)
 | ⟨h_ginj, h_gsurj⟩ ⟨h_finj, h_fsurj⟩ := ⟨injective_comp h_ginj h_finj, surjective_comp h_gsurj h_fsurj⟩
 
--- g is a left inverse to f
+/-- `left_inverse g f` means that g is a left inverse to f. That is, `g ∘ f = id`. -/
 def left_inverse (g : β → α) (f : α → β) : Prop := ∀ x, g (f x) = x
 
 def has_left_inverse (f : α → β) : Prop := ∃ finv : β → α, left_inverse finv f
 
--- g is a right inverse to f
+/-- `right_inverse g f` means that g is a right inverse to f. That is, `f ∘ g = id`. -/
 def right_inverse (g : β → α) (f : α → β) : Prop := left_inverse f g
 
 def has_right_inverse (f : α → β) : Prop := ∃ finv : β → α, right_inverse finv f

library/init/logic.lean

@@ -25,12 +25,14 @@ assume hp, h₂ (h₁ hp)
 
 def trivial : true := ⟨⟩
 
+/-- We can't have `a` and `¬a`, that would be absurd!-/
 @[inline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) : b :=
 false.rec b (h₂ h₁)
 
 lemma not.intro {a : Prop} (h : a → false) : ¬ a :=
 h
 
+/-- Modus tollens.-/
 lemma mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a := assume ha : a, h₂ (h₁ ha)
 
 /- not -/
@@ -626,7 +628,7 @@ namespace decidable
   decidable.rec_on h (λ h, h₄) (λ h, false.rec _ (h₃ h))
 
   def by_cases {q : Sort u} [φ : decidable p] : (p → q) → (¬p → q) → q := dite _
-
+  /-- Law of Excluded Middle. -/
   lemma em (p : Prop) [decidable p] : p ∨ ¬p := by_cases or.inl or.inr
 
   lemma by_contradiction [decidable p] (h : ¬p → false) : p :=