feat(logic/basic): introduce pempty

leanprover-community · Aug 29, 2018 · f903d20 · f903d20
1 parent 0c11112
commit f903d20
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 0 deletions.
diff --git a/data/fintype.lean b/data/fintype.lean
@@ -169,6 +169,12 @@ instance : fintype empty := ⟨∅, empty.rec _⟩
 
 @[simp] theorem fintype.card_empty : fintype.card empty = 0 := rfl
 
+instance : fintype pempty := ⟨∅, pempty.rec _⟩
+
+@[simp] theorem fintype.univ_pempty : @univ pempty _ = ∅ := rfl
+
+@[simp] theorem fintype.card_pempty : fintype.card pempty = 0 := rfl
+
 instance : fintype unit := ⟨⟨()::0, by simp⟩, λ ⟨⟩, by simp⟩
 
 @[simp] theorem fintype.univ_unit : @univ unit _ = {()} := rfl

diff --git a/logic/basic.lean b/logic/basic.lean
@@ -37,6 +37,9 @@ instance : decidable_eq empty := λa, a.elim
 @[simp] theorem coe_coe {α β γ} [has_coe α β] [has_coe_t β γ]
   (a : α) : (a : γ) = (a : β) := rfl
 
+@[derive decidable_eq]
+inductive {u} pempty : Type u
+
 end miscellany
 
 /-