From 5b7fb1f61a76574c291d711c52d993241c7a6963 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Fri, 15 Aug 2014 13:04:32 -0700 Subject: [PATCH] feat(library/standard/classes): add nonempty --- library/standard/logic/classes/nonempty.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 library/standard/logic/classes/nonempty.lean diff --git a/library/standard/logic/classes/nonempty.lean b/library/standard/logic/classes/nonempty.lean new file mode 100644 index 000000000..11c0fd5b2 --- /dev/null +++ b/library/standard/logic/classes/nonempty.lean @@ -0,0 +1,14 @@ +-- Copyright (c) 2014 Microsoft Corporation. All rights reserved. +-- Released under Apache 2.0 license as described in the file LICENSE. +-- Authors: Leonardo de Moura, Jeremy Avigad + +import logic.connectives.basic .inhabited + +inductive nonempty (A : Type) : Prop := +| nonempty_intro : A → nonempty A + +definition nonempty_elim {A : Type} {B : Type} (H1 : nonempty A) (H2 : A → B) : B := +nonempty_rec H2 H1 + +theorem inhabited_imp_nonempty [instance] {A : Type} (H : inhabited A) : nonempty A := +nonempty_intro (default A)