chore(library/init): convert /- comments to /-- or /-! comments (…

…#782)

This isn't exhaustive, but converts the majority.
It also does not check that the comments have reasonable markdown formatting.

library/init/cc_lemmas.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import init.propext init.classical
 
-/- Lemmas use by the congruence closure module -/
+/-! Lemmas use by the congruence closure module -/
 
 lemma iff_eq_of_eq_true_left {a b : Prop} (h : a = true) : (a ↔ b) = b :=
 h.symm ▸ propext (true_iff _)
@@ -58,7 +58,7 @@ h.symm ▸ propext (iff.intro (λ h, trivial) (λ h₁ h₂, false.elim h₂))
 lemma imp_eq_of_eq_false_right {a b : Prop} (h : b = false) : (a → b) = not a :=
 h.symm ▸ propext (iff.intro (λ h, h) (λ hna ha, hna ha))
 
-/- Remark: the congruence closure module will only use the following lemma is
+/-- Remark: the congruence closure module will only use this lemma if
    cc_config.em is tt. -/
 lemma not_imp_eq_of_eq_false_right {a b : Prop} (h : b = false) : (not a → b) = a :=
 h.symm ▸ propext (iff.intro (λ h', classical.by_contradiction (λ hna, h' hna)) (λ ha hna, hna ha))
@@ -105,7 +105,7 @@ eq_false_intro (λ hb, false.elim (eq.mp h (or.inr hb)))
 lemma eq_false_of_not_eq_true {a : Prop} (h : (not a) = true) : a = false :=
 eq_false_intro (λ ha, absurd ha (eq.mpr h trivial))
 
-/- Remark: the congruence closure module will only use the following lemma is
+/-- Remark: the congruence closure module will only use this lemma if
    cc_config.em is tt. -/
 lemma eq_true_of_not_eq_false {a : Prop} (h : (not a) = false) : a = true :=
 eq_true_intro (classical.by_contradiction (λ hna, eq.mp h hna))

library/init/classical.lean

@@ -9,7 +9,7 @@ import init.data.subtype.basic init.funext
 namespace classical
 universes u v
 
-/- the axiom -/
+/-- The axiom -/
 axiom choice {α : Sort u} : nonempty α → α
 
 @[irreducible] noncomputable def indefinite_description {α : Sort u} (p : α → Prop)
@@ -79,7 +79,7 @@ noncomputable def inhabited_of_exists {α : Sort u} {p : α → Prop} (h : ∃ x
   inhabited α :=
 inhabited_of_nonempty (exists.elim h (λ w hw, ⟨w⟩))
 
-/- all propositions are decidable -/
+/-- All propositions are decidable -/
 noncomputable def prop_decidable (a : Prop) : decidable a :=
 choice $ or.elim (em a)
   (assume ha, ⟨is_true ha⟩)
@@ -106,8 +106,7 @@ if hp : ∃ x : α, p x then
   ⟨xp.val, λ h', xp.property⟩
 else ⟨choice h, λ h, absurd h hp⟩
 
-/- the Hilbert epsilon function -/
-
+/-- The Hilbert epsilon function -/
 noncomputable def epsilon {α : Sort u} [h : nonempty α] (p : α → Prop) : α :=
 (strong_indefinite_description p h).val
 
@@ -122,7 +121,7 @@ epsilon_spec_aux (nonempty_of_exists hex) p hex
 theorem epsilon_singleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (λ y, y = x) = x :=
 @epsilon_spec α (λ y, y = x) ⟨x, rfl⟩
 
-/- the axiom of choice -/
+/-- The axiom of choice -/
 
 theorem axiom_of_choice {α : Sort u} {β : α → Sort v} {r : Π x, β x → Prop} (h : ∀ x, ∃ y, r x y) :
   ∃ (f : Π x, β x), ∀ x, r x (f x) :=

library/init/control/monad.lean

@@ -27,6 +27,6 @@ class monad (m : Type u → Type v) extends applicative m, has_bind m : Type (ma
 @[reducible, inline] def return {m : Type u → Type v} [monad m] {α : Type u} : α → m α :=
 pure
 
-/- Identical to has_bind.and_then, but it is not inlined. -/
+/-- Identical to `has_bind.and_then`, but it is not inlined. -/
 def has_bind.seq {α β : Type u} {m : Type u → Type v} [has_bind m] (x : m α) (y : m β) : m β :=
 do x, y

library/init/core.lean

@@ -36,7 +36,7 @@ a
 /-- Gadget for marking output parameters in type classes. -/
 @[reducible] def out_param (α : Sort u) : Sort u := α
 
-/-
+/--
   id_rhs is an auxiliary declaration used in the equation compiler to address performance
   issues when proving equational lemmas. The equation compiler uses it as a marker.
 -/
@@ -88,9 +88,9 @@ prefix `¬`:40 := not
 inductive eq {α : Sort u} (a : α) : α → Prop
 | refl [] : eq a
 
-/-
+/-!
 Initialize the quotient module, which effectively adds the following definitions:
-
+```lean
 constant quot {α : Sort u} (r : α → α → Prop) : Sort u
 
 constant quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : quot r
@@ -100,11 +100,11 @@ 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
 
@@ -243,7 +243,7 @@ inductive bool : Type
 | ff : bool
 | tt : bool
 
-/- Remark: subtype must take a Sort instead of Type because of the axiom strong_indefinite_description. -/
+/-- Remark: subtype must take a Sort instead of Type because of the axiom strong_indefinite_description. -/
 structure subtype {α : Sort u} (p : α → Prop) :=
 (val : α) (property : p val)
 
@@ -293,7 +293,7 @@ structure unification_hint :=
 (pattern : unification_constraint)
 (constraints : list unification_constraint)
 
-/- Declare builtin and reserved notation -/
+/-! Declare builtin and reserved notation -/
 
 class has_zero     (α : Type u) := (zero : α)
 class has_one      (α : Type u) := (one : α)
@@ -323,10 +323,10 @@ class has_ssubset  (α : Type u) := (ssubset : α → α → Prop)
 class has_emptyc   (α : Type u) := (emptyc : α)
 class has_insert   (α : out_param $ Type u) (γ : Type v) := (insert : α → γ → γ)
 class has_singleton (α : out_param $ Type u) (β : Type v) := (singleton : α → β)
-/- Type class used to implement the notation { a ∈ c | p a } -/
+/-- Type class used to implement the notation { a ∈ c | p a } -/
 class has_sep (α : out_param $ Type u) (γ : Type v) :=
 (sep : (α → Prop) → γ → γ)
-/- Type class for set-like membership -/
+/-- Type class for set-like membership -/
 class has_mem (α : out_param $ Type u) (γ : Type v) := (mem : α → γ → Prop)
 
 class has_pow (α : Type u) (β : Type v) :=
@@ -389,7 +389,7 @@ export is_lawful_singleton (insert_emptyc_eq)
 
 attribute [simp] insert_emptyc_eq
 
-/- nat basic instances -/
+/-! nat basic instances -/
 
 namespace nat
   protected def add : nat → nat → nat
@@ -425,11 +425,10 @@ end nat
 def std.prec.max   : nat := 1024 -- the strength of application, identifiers, (, [, etc.
 def std.prec.arrow : nat := 25
 
-/-
-The next def is "max + 10". It can be used e.g. for postfix operations that should
+/--
+This def is "max + 10". It can be used e.g. for postfix operations that should
 be stronger than application.
 -/
-
 def std.prec.max_plus : nat := std.prec.max + 10
 
 postfix `⁻¹`:std.prec.max_plus := has_inv.inv  -- input with \sy or \-1 or \inv
@@ -445,12 +444,12 @@ class has_sizeof (α : Sort u) :=
 def sizeof {α : Sort u} [s : has_sizeof α] : α → nat :=
 has_sizeof.sizeof
 
-/-
+/-!
 Declare sizeof instances and lemmas for types declared before has_sizeof.
 From now on, the inductive compiler will automatically generate sizeof instances and lemmas.
 -/
 
-/- Every type `α` has a default has_sizeof instance that just returns 0 for every element of `α` -/
+/-- Every type `α` has a default has_sizeof instance that just returns 0 for every element of `α` -/
 protected def default.sizeof (α : Sort u) : α → nat
 | a := 0
 

library/init/data/int/basic.lean

@@ -2,14 +2,15 @@
 Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
-
-The integers, with addition, multiplication, and subtraction.
 -/
 prelude
 import init.data.nat.lemmas init.data.nat.gcd
 open nat
 
-/- the type, coercions, and notation -/
+/-!
+# The integers, with addition, multiplication, and subtraction.
+
+the type, coercions, and notation -/
 
 @[derive decidable_eq]
 inductive int : Type
@@ -46,7 +47,7 @@ lemma of_nat_zero : of_nat (0 : nat) = (0 : int) := rfl
 
 lemma of_nat_one : of_nat (1 : nat) = (1 : int) := rfl
 
-/- definitions of basic functions -/
+/-! definitions of basic functions -/
 
 def neg_of_nat : ℕ → ℤ
 | 0        := 0
@@ -115,7 +116,7 @@ protected lemma coe_nat_add_out (m n : ℕ) : ↑m + ↑n = (m + n : ℤ) := rfl
 protected lemma coe_nat_mul_out (m n : ℕ) : ↑m * ↑n = (↑(m * n) : ℤ) := rfl
 protected lemma coe_nat_add_one_out (n : ℕ) : ↑n + (1 : ℤ) = ↑(succ n) := rfl
 
-/- these are only for internal use -/
+/-! these are only for internal use -/
 
 lemma of_nat_add_of_nat (m n : nat) : of_nat m + of_nat n = of_nat (m + n) := rfl
 lemma of_nat_add_neg_succ_of_nat (m n : nat) :
@@ -138,7 +139,7 @@ local attribute [simp] of_nat_add_of_nat of_nat_mul_of_nat neg_of_nat_zero neg_o
   neg_succ_of_nat_add_neg_succ_of_nat of_nat_mul_neg_succ_of_nat neg_succ_of_nat_of_nat
   mul_neg_succ_of_nat_neg_succ_of_nat
 
-/- some basic functions and properties -/
+/-!  some basic functions and properties -/
 
 protected lemma coe_nat_inj {m n : ℕ} (h : (↑m : ℤ) = ↑n) : m = n :=
 int.of_nat.inj h
@@ -154,7 +155,7 @@ lemma neg_succ_of_nat_inj_iff {m n : ℕ} : neg_succ_of_nat m = neg_succ_of_nat
 
 lemma neg_succ_of_nat_eq (n : ℕ) : -[1+ n] = -(n + 1) := rfl
 
-/- neg -/
+/-! neg -/
 
 protected lemma neg_neg : ∀ a : ℤ, -(-a) = a
 | (of_nat 0)     := rfl
@@ -166,7 +167,7 @@ by rw [← int.neg_neg a, ← int.neg_neg b, h]
 
 protected lemma sub_eq_add_neg {a b : ℤ} : a - b = a + -b := rfl
 
-/- basic properties of sub_nat_nat -/
+/-! basic properties of sub_nat_nat -/
 
 lemma sub_nat_nat_elim (m n : ℕ) (P : ℕ → ℕ → ℤ → Prop)
   (hp : ∀i n, P (n + i) n (of_nat i))
@@ -220,7 +221,7 @@ lemma sub_nat_nat_of_lt {m n : ℕ} (h : m < n) : sub_nat_nat m n = -[1+ pred (n
 have n - m = succ (pred (n - m)), from eq.symm (succ_pred_eq_of_pos (nat.sub_pos_of_lt h)),
 by rewrite sub_nat_nat_of_sub_eq_succ this
 
-/- nat_abs -/
+/-! nat_abs -/
 
 @[simp] def nat_abs : ℤ → ℕ
 | (of_nat m) := m
@@ -252,7 +253,7 @@ lemma nat_abs_eq : Π (a : ℤ), a = nat_abs a ∨ a = -(nat_abs a)
 
 lemma eq_coe_or_neg (a : ℤ) : ∃n : ℕ, a = n ∨ a = -n := ⟨_, nat_abs_eq a⟩
 
-/- sign -/
+/-! sign -/
 
 def sign : ℤ → ℤ
 | (n+1:ℕ) := 1
@@ -263,7 +264,7 @@ def sign : ℤ → ℤ
 @[simp] theorem sign_one : sign 1 = 1 := rfl
 @[simp] theorem sign_neg_one : sign (-1) = -1 := rfl
 
-/- Quotient and remainder -/
+/-! Quotient and remainder -/
 
 -- There are three main conventions for integer division,
 -- referred here as the E, F, T rounding conventions.
@@ -314,15 +315,15 @@ def rem : ℤ → ℤ → ℤ
 instance : has_div ℤ := ⟨int.div⟩
 instance : has_mod ℤ := ⟨int.mod⟩
 
-/- gcd -/
+/-! gcd -/
 
 def gcd (m n : ℤ) : ℕ := gcd (nat_abs m) (nat_abs n)
 
 /-
    int is a ring
 -/
 
-/- addition -/
+/-! addition -/
 
 protected lemma add_comm : ∀ a b : ℤ, a + b = b + a
 | (of_nat n) (of_nat m) := by simp [nat.add_comm]
@@ -394,7 +395,7 @@ protected lemma add_assoc : ∀ a b c : ℤ, a + b + c = a + (b + c)
                                          int.add_comm -[1+ k] ]
 | -[1+ m]    -[1+ n]    -[1+ k]    := by simp [add_succ, nat.add_comm, nat.add_left_comm, neg_of_nat_of_succ]
 
-/- negation -/
+/-! negation -/
 
 lemma sub_nat_self : ∀ n, sub_nat_nat n n = 0
 | 0        := rfl
@@ -410,7 +411,7 @@ protected lemma add_left_neg : ∀ a : ℤ, -a + a = 0
 protected lemma add_right_neg (a : ℤ) : a + -a = 0 :=
 by rw [int.add_comm, int.add_left_neg]
 
-/- multiplication -/
+/-! multiplication -/
 
 protected lemma mul_comm : ∀ a b : ℤ, a * b = b * a
 | (of_nat m) (of_nat n) := by simp [nat.mul_comm]

library/init/data/int/comp_lemmas.lean

@@ -2,16 +2,16 @@
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
-
-Auxiliary lemmas used to compare int numerals.
 -/
 prelude
 import init.data.int.order
 
 namespace int
-/- Auxiliary lemmas for proving that to int numerals are different -/
+/-!
+# Auxiliary lemmas for proving that two int numerals are differen
+-/
 
-/- 1. Lemmas for reducing the problem to the case where the numerals are positive -/
+/-! 1. Lemmas for reducing the problem to the case where the numerals are positive -/
 
 protected lemma ne_neg_of_ne {a b : ℤ} : a ≠ b → -a ≠ -b :=
 λ h₁ h₂, absurd (int.neg_inj h₂) h₁
@@ -37,7 +37,7 @@ end
 protected lemma ne_neg_of_pos {a b : ℤ} : 0 < a → 0 < b → a ≠ -b :=
 λ h₁ h₂, ne.symm (int.neg_ne_of_pos h₂ h₁)
 
-/- 2. Lemmas for proving that positive int numerals are nonneg and positive -/
+/-! 2. Lemmas for proving that positive int numerals are nonneg and positive -/
 
 protected lemma one_pos : 0 < (1:int) :=
 int.zero_lt_one
@@ -63,7 +63,7 @@ protected lemma bit1_nonneg {a : ℤ} : 0 ≤ a → 0 ≤ bit1 a :=
 protected lemma nonneg_of_pos {a : ℤ} : 0 < a → 0 ≤ a :=
 le_of_lt
 
-/- 3. nat_abs auxiliary lemmas -/
+/-! 3. nat_abs auxiliary lemmas -/
 
 lemma neg_succ_of_nat_lt_zero (n : ℕ) : neg_succ_of_nat n < 0 :=
 @lt.intro _ _ n (by simp [neg_succ_of_nat_coe, int.coe_nat_succ, int.coe_nat_add, int.coe_nat_one,
@@ -88,7 +88,7 @@ protected lemma ne_of_nat_ne_nonneg_case {a b : ℤ} {n m : nat} (ha : 0 ≤ a)
 have nat_abs a ≠ nat_abs b, by rwa [e1, e2],
 ne_of_nat_abs_ne_nat_abs_of_nonneg ha hb this
 
-/- 4. Aux lemmas for pushing nat_abs inside numerals
+/-! 4. Aux lemmas for pushing nat_abs inside numerals
    nat_abs_zero and nat_abs_one are defined at init/data/int/basic.lean -/
 
 lemma nat_abs_of_nat_core (n : ℕ) : nat_abs (of_nat n) = n :=

library/init/data/int/order.lean

@@ -107,7 +107,7 @@ lemma lt_of_coe_nat_lt_coe_nat {m n : ℕ} (h : (↑m : ℤ) < ↑n) : m < n :=
 lemma coe_nat_lt_coe_nat_of_lt {m n : ℕ} (h : m < n) : (↑m : ℤ) < ↑n :=
 (coe_nat_lt_coe_nat_iff _ _).mpr h
 
-/- show that the integers form an ordered additive group -/
+/-! show that the integers form an ordered additive group -/
 
 protected lemma le_refl (a : ℤ) : a ≤ a :=
 le.intro (int.add_zero a)
@@ -215,7 +215,7 @@ lemma eq_neg_succ_of_lt_zero : ∀ {a : ℤ}, a < 0 → ∃ n : ℕ, a = -[1+ n]
 | (n : ℕ) h := absurd h (not_lt_of_ge (coe_zero_le _))
 | -[1+ n] h := ⟨n, rfl⟩
 
-/- int is an ordered add comm group -/
+/-! int is an ordered add comm group -/
 
 protected lemma eq_neg_of_eq_neg {a b : ℤ} (h : a = -b) : b = -a :=
 by rw [h, int.neg_neg]
@@ -771,7 +771,7 @@ end
 
 end
 
-/- missing facts -/
+/-! missing facts -/
 
 protected lemma mul_lt_mul_of_pos_left {a b c : ℤ}
        (h₁ : a < b) (h₂ : 0 < c) : c * a < c * b :=
@@ -874,7 +874,7 @@ int.mul_le_mul h2 h2 h1 (le_trans h1 h2)
 protected lemma mul_self_lt_mul_self {a b : ℤ} (h1 : 0 ≤ a) (h2 : a < b) : a * a < b * b :=
 int.mul_lt_mul' (le_of_lt h2) h2 h1 (lt_of_le_of_lt h1 h2)
 
-/- more facts specific to int -/
+/-! more facts specific to int -/
 
 theorem of_nat_nonneg (n : ℕ) : 0 ≤ of_nat n := trivial