From d2a4bb8a276348c5a42d7add7cd27e3eeba585a1 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 5 Sep 2014 09:31:27 -0700 Subject: [PATCH] feat(library/data/empty): add false.to_empty and false.rec_type theorems Signed-off-by: Leonardo de Moura --- library/data/empty.lean | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/library/data/empty.lean b/library/data/empty.lean index 6b19b4e00..50f9299c1 100644 --- a/library/data/empty.lean +++ b/library/data/empty.lean @@ -1,15 +1,23 @@ -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Jeremy Avigad - --- TODO: add notation for negation (in the sense of homotopy type theory) +-- Author: Jeremy Avigad, Floris van Doorn -- Empty type -- ---------- +import logic.core.cast + inductive empty : Type namespace empty theorem elim [protected] (A : Type) (H : empty) : A := rec (λe, A) H end empty + +namespace false + theorem to_empty (H : false) : empty := + cast (false_elim H) true + + theorem rec_type (A : Type) (H : false) : A := + empty.rec (λx,A) (to_empty H) +end false