From d42fd657fe1a3b6dbb9bcbe8a64d716e1a36859a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Oct 2014 09:00:34 -0700 Subject: [PATCH] refactor(library): is_inhabited "theorems" should be "definitions", they are "data" --- library/data/bool.lean | 2 +- library/data/nat/basic.lean | 2 +- library/data/num.lean | 4 ++-- library/data/option.lean | 2 +- library/data/prod.lean | 2 +- library/data/sigma.lean | 2 +- library/data/string.lean | 4 ++-- library/data/subtype.lean | 2 +- library/data/sum.lean | 4 ++-- library/data/unit.lean | 2 +- library/data/vector.lean | 2 +- 11 files changed, 14 insertions(+), 14 deletions(-) diff --git a/library/data/bool.lean b/library/data/bool.lean index f3176c36a8..1b5fb5eb0d 100644 --- a/library/data/bool.lean +++ b/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 := diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index 6e9980ac29..30ec6cf2ed 100644 --- a/library/data/nat/basic.lean +++ b/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 diff --git a/library/data/num.lean b/library/data/num.lean index 87c7cf54e2..961c4fc05e 100644 --- a/library/data/num.lean +++ b/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 diff --git a/library/data/option.lean b/library/data/option.lean index 87314d7a7f..a289bd9190 100644 --- a/library/data/option.lean +++ b/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) := diff --git a/library/data/prod.lean b/library/data/prod.lean index e2d09e44b0..1e50f26fef 100644 --- a/library/data/prod.lean +++ b/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) := diff --git a/library/data/sigma.lean b/library/data/sigma.lean index e346b75237..ef45bfbfbc 100644 --- a/library/data/sigma.lean +++ 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 diff --git a/library/data/string.lean b/library/data/string.lean index d811a48abe..b82f768e7d 100644 --- a/library/data/string.lean +++ b/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 diff --git a/library/data/subtype.lean b/library/data/subtype.lean index 3e217a162d..2dff44a116 100644 --- a/library/data/subtype.lean +++ b/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} := diff --git a/library/data/sum.lean b/library/data/sum.lean index 8fba4a15ed..ee628eb688 100644 --- a/library/data/sum.lean +++ b/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) : diff --git a/library/data/unit.lean b/library/data/unit.lean index aee94ce84c..b768cfee62 100644 --- a/library/data/unit.lean +++ 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 := diff --git a/library/data/vector.lean b/library/data/vector.lean index 9214e44102..c6e14b056d 100644 --- a/library/data/vector.lean +++ b/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)),