michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/data/empty): add false.to_empty and false.rec_type theorems

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Floris van Doorn 2014-09-05 09:31:27 -07:00 committed by Leonardo de Moura
parent db60a56056
commit d2a4bb8a27
1 changed files with 11 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
library/data/empty.lean
View file

@ -1,15 +1,23 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE. -- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jeremy Avigad -- Author: Jeremy Avigad, Floris van Doorn
-- TODO: add notation for negation (in the sense of homotopy type theory)
-- Empty type -- Empty type
-- ---------- -- ----------
import logic.core.cast
inductive empty : Type inductive empty : Type
namespace empty namespace empty
theorem elim [protected] (A : Type) (H : empty) : A := theorem elim [protected] (A : Type) (H : empty) : A :=
rec (λe, A) H rec (λe, A) H
end empty 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