refactor(library): is_inhabited "theorems" should be "definitions", they are "data"

library/data/bool.lean

@@ -133,7 +133,7 @@ namespace bool
   theorem bnot_true  : not tt = ff :=
   rfl
 
-  protected theorem is_inhabited [instance] : inhabited bool :=
+  protected definition is_inhabited [instance] : inhabited bool :=
   inhabited.mk ff
 
   protected definition has_decidable_eq [instance] : decidable_eq bool :=

library/data/nat/basic.lean

@@ -37,7 +37,7 @@ nat.rec H1 H2 a
 protected definition rec_on {P : ℕ → Type} (n : ℕ) (H1 : P zero) (H2 : ∀m, P m → P (succ m)) : P n :=
 nat.rec H1 H2 n
 
-protected theorem is_inhabited [instance] : inhabited nat :=
+protected definition is_inhabited [instance] : inhabited nat :=
 inhabited.mk zero
 
 -- Coercion from num

library/data/num.lean

@@ -14,7 +14,7 @@ one  : pos_num,
 bit1 : pos_num → pos_num,
 bit0 : pos_num → pos_num
 
-theorem pos_num.is_inhabited [instance] : inhabited pos_num :=
+definition pos_num.is_inhabited [instance] : inhabited pos_num :=
 inhabited.mk pos_num.one
 
 namespace pos_num
@@ -120,7 +120,7 @@ inductive num : Type :=
 zero  : num,
 pos   : pos_num → num
 
-theorem num.is_inhabited [instance] : inhabited num :=
+definition num.is_inhabited [instance] : inhabited num :=
 inhabited.mk num.zero
 
 namespace num

library/data/option.lean

@@ -35,7 +35,7 @@ namespace option
   protected theorem equal {A : Type} {a₁ a₂ : A} (H : some a₁ = some a₂) : a₁ = a₂ :=
   congr_arg (option.rec a₁ (λ a, a)) H
 
-  protected theorem is_inhabited [instance] (A : Type) : inhabited (option A) :=
+  protected definition is_inhabited [instance] (A : Type) : inhabited (option A) :=
   inhabited.mk none
 
   protected definition has_decidable_eq [instance] {A : Type} (H : decidable_eq A) : decidable_eq (option A) :=

library/data/prod.lean

@@ -45,7 +45,7 @@ section
   protected theorem equal {p1 p2 : prod A B} : ∀ (H1 : pr1 p1 = pr1 p2) (H2 : pr2 p1 = pr2 p2), p1 = p2 :=
   destruct p1 (take a1 b1, destruct p2 (take a2 b2 H1 H2, pair_eq H1 H2))
 
-  protected theorem is_inhabited [instance] (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) :=
+  protected definition is_inhabited [instance] (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) :=
   inhabited.destruct H1 (λa, inhabited.destruct H2 (λb, inhabited.mk (pair a b)))
 
   protected definition has_decidable_eq [instance] (H1 : decidable_eq A) (H2 : decidable_eq B) : decidable_eq (A × B) :=

library/data/sigma.lean

@@ -33,7 +33,7 @@ section
     ∀(H₁ : dpr1 p₁ = dpr1 p₂) (H₂ : eq.rec_on H₁ (dpr2 p₁) = dpr2 p₂), p₁ = p₂ :=
   destruct p₁ (take a₁ b₁, destruct p₂ (take a₂ b₂ H₁ H₂, dpair_eq H₁ H₂))
 
-  protected theorem is_inhabited [instance] (H₁ : inhabited A) (H₂ : inhabited (B (default A))) :
+  protected definition is_inhabited [instance] (H₁ : inhabited A) (H₂ : inhabited (B (default A))) :
     inhabited (sigma B) :=
   inhabited.destruct H₁ (λa, inhabited.destruct H₂ (λb, inhabited.mk (dpair (default A) b)))
 end

library/data/string.lean

@@ -10,7 +10,7 @@ inductive char : Type :=
   mk : bool → bool → bool → bool → bool → bool → bool → bool → char
 
 namespace char
-  protected theorem is_inhabited [instance] : inhabited char :=
+  protected definition is_inhabited [instance] : inhabited char :=
   inhabited.mk (mk ff ff ff ff ff ff ff ff)
 end char
 
@@ -19,6 +19,6 @@ inductive string : Type :=
   str   : char → string → string
 
 namespace string
-  protected theorem is_inhabited [instance] : inhabited string :=
+  protected definition is_inhabited [instance] : inhabited string :=
   inhabited.mk empty
 end string

library/data/subtype.lean

@@ -38,7 +38,7 @@ section
   protected theorem equal {a1 a2 : {x, P x}} : ∀(H : elt_of a1 = elt_of a2), a1 = a2 :=
   destruct a1 (take x1 H1, destruct a2 (take x2 H2 H, tag_eq H))
 
-  protected theorem is_inhabited [instance] {a : A} (H : P a) : inhabited {x, P x} :=
+  protected definition is_inhabited [instance] {a : A} (H : P a) : inhabited {x, P x} :=
   inhabited.mk (tag a H)
 
   protected definition has_decidable_eq [instance] (H : decidable_eq A) : decidable_eq {x, P x} :=

library/data/sum.lean

@@ -49,10 +49,10 @@ namespace sum
   have H2 : f (inr A b2), from H ▸ H1,
   H2
 
-  protected theorem is_inhabited_left [instance] {A B : Type} (H : inhabited A) : inhabited (A ⊎ B) :=
+  protected definition is_inhabited_left [instance] {A B : Type} (H : inhabited A) : inhabited (A ⊎ B) :=
   inhabited.mk (inl B (default A))
 
-  protected theorem is_inhabited_right [instance] {A B : Type} (H : inhabited B) : inhabited (A ⊎ B) :=
+  protected definition is_inhabited_right [instance] {A B : Type} (H : inhabited B) : inhabited (A ⊎ B) :=
   inhabited.mk (inr A (default B))
 
   protected definition has_eq_decidable [instance] {A B : Type} (H1 : decidable_eq A) (H2 : decidable_eq B) :

library/data/unit.lean

@@ -15,7 +15,7 @@ namespace unit
   theorem eq_star (a : unit) : a = star :=
   equal a star
 
-  protected theorem is_inhabited [instance] : inhabited unit :=
+  protected definition is_inhabited [instance] : inhabited unit :=
   inhabited.mk ⋆
 
   protected definition has_decidable_eq [instance] : decidable_eq unit :=

library/data/vector.lean

@@ -27,7 +27,7 @@ namespace vector
     (Hcons : ∀(x : T) {n : ℕ} (w : vector T n), C (succ n) (cons x w)) : C n v :=
   rec_on v Hnil (take x n v IH, Hcons x v)
 
-  protected theorem is_inhabited [instance] (A : Type) (H : inhabited A) (n : nat) : inhabited (vector A n) :=
+  protected definition is_inhabited [instance] (A : Type) (H : inhabited A) (n : nat) : inhabited (vector A n) :=
   nat.rec_on n
     (inhabited.mk (@vector.nil A))
     (λ (n : nat) (iH : inhabited (vector A n)),