From e587449a6d26b4af003499467a0b84bf9dea62c1 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Tue, 23 Dec 2014 15:35:06 -0500 Subject: [PATCH] refactor(library/data): remove folders with a single file --- library/data/{bool/thms.lean => bool.lean} | 2 +- library/data/bool/default.lean | 9 ------ library/data/data.md | 4 +-- library/data/empty.lean | 12 ++++---- library/data/{num/thms.lean => num.lean} | 2 +- library/data/num/default.lean | 9 ------ library/data/{prod/thms.lean => prod.lean} | 11 ++++++-- library/data/prod/default.lean | 4 --- library/data/{sigma/thms.lean => sigma.lean} | 0 library/data/sigma/default.lean | 4 --- .../data/{string/thms.lean => string.lean} | 11 ++++++-- library/data/string/default.lean | 4 --- library/data/unit.lean | 28 +++++++++++++++++++ library/data/unit/default.lean | 7 ----- library/data/unit/insts.lean | 16 ----------- library/data/unit/thms.lean | 12 -------- 16 files changed, 55 insertions(+), 80 deletions(-) rename library/data/{bool/thms.lean => bool.lean} (99%) delete mode 100644 library/data/bool/default.lean rename library/data/{num/thms.lean => num.lean} (98%) delete mode 100644 library/data/num/default.lean rename library/data/{prod/thms.lean => prod.lean} (95%) delete mode 100644 library/data/prod/default.lean rename library/data/{sigma/thms.lean => sigma.lean} (100%) delete mode 100644 library/data/sigma/default.lean rename library/data/{string/thms.lean => string.lean} (61%) delete mode 100644 library/data/string/default.lean create mode 100644 library/data/unit.lean delete mode 100644 library/data/unit/default.lean delete mode 100644 library/data/unit/insts.lean delete mode 100644 library/data/unit/thms.lean diff --git a/library/data/bool/thms.lean b/library/data/bool.lean similarity index 99% rename from library/data/bool/thms.lean rename to library/data/bool.lean index 5b1242b31..cd5dfda84 100644 --- a/library/data/bool/thms.lean +++ b/library/data/bool.lean @@ -2,7 +2,7 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Module: data.bool.thms +Module: data.bool Author: Leonardo de Moura -/ diff --git a/library/data/bool/default.lean b/library/data/bool/default.lean deleted file mode 100644 index f5d128100..000000000 --- a/library/data/bool/default.lean +++ /dev/null @@ -1,9 +0,0 @@ -/- -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.bool.default -Author: Leonardo de Moura --/ - -import data.bool.thms diff --git a/library/data/data.md b/library/data/data.md index c3cb7a132..2e4274a27 100644 --- a/library/data/data.md +++ b/library/data/data.md @@ -7,8 +7,8 @@ Basic types: * [empty](empty.lean) : the empty type * [unit](unit.lean) : the singleton type -* [bool](bool/bool.md) : the boolean values -* [num](num/num.md) : generic numerals +* [bool](bool.lean) : the boolean values +* [num](num.lean) : generic numerals * [string](string.lean) : ascii strings * [nat](nat/nat.md) : the natural numbers * [fin](fin.lean) : finite ordinals diff --git a/library/data/empty.lean b/library/data/empty.lean index d9f398127..c3ed86852 100644 --- a/library/data/empty.lean +++ b/library/data/empty.lean @@ -1,9 +1,11 @@ --- Copyright (c) 2014 Microsoft Corporation. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Jeremy Avigad, Floris van Doorn +/- +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: data.empty +Author: Jeremy Avigad, Floris van Doorn +-/ --- Empty type --- ---------- import logic.cast logic.subsingleton namespace empty diff --git a/library/data/num/thms.lean b/library/data/num.lean similarity index 98% rename from library/data/num/thms.lean rename to library/data/num.lean index f40093bb0..01f68a9bb 100644 --- a/library/data/num/thms.lean +++ b/library/data/num.lean @@ -2,7 +2,7 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Module: data.num.thms +Module: data.num Author: Leonardo de Moura -/ diff --git a/library/data/num/default.lean b/library/data/num/default.lean deleted file mode 100644 index 79e821538..000000000 --- a/library/data/num/default.lean +++ /dev/null @@ -1,9 +0,0 @@ -/- -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.num.default -Author: Leonardo de Moura --/ - -import data.num.thms diff --git a/library/data/prod/thms.lean b/library/data/prod.lean similarity index 95% rename from library/data/prod/thms.lean rename to library/data/prod.lean index 3c4886137..c1e5e5a7c 100644 --- a/library/data/prod/thms.lean +++ b/library/data/prod.lean @@ -1,6 +1,11 @@ --- Copyright (c) 2014 Microsoft Corporation. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Leonardo de Moura, Jeremy Avigad +/- +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: data.prod +Author: Leonardo de Moura, Jeremy Avigad +-/ + import logic.eq open inhabited decidable eq.ops diff --git a/library/data/prod/default.lean b/library/data/prod/default.lean deleted file mode 100644 index 968cf5aee..000000000 --- a/library/data/prod/default.lean +++ /dev/null @@ -1,4 +0,0 @@ --- Copyright (c) 2014 Microsoft Corporation. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Leonardo de Moura, Jeremy Avigad -import data.prod.thms diff --git a/library/data/sigma/thms.lean b/library/data/sigma.lean similarity index 100% rename from library/data/sigma/thms.lean rename to library/data/sigma.lean diff --git a/library/data/sigma/default.lean b/library/data/sigma/default.lean deleted file mode 100644 index b2ab21f7f..000000000 --- a/library/data/sigma/default.lean +++ /dev/null @@ -1,4 +0,0 @@ --- Copyright (c) 2014 Microsoft Corporation. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn -import data.sigma.thms diff --git a/library/data/string/thms.lean b/library/data/string.lean similarity index 61% rename from library/data/string/thms.lean rename to library/data/string.lean index 2858b8bab..1e0a738e6 100644 --- a/library/data/string/thms.lean +++ b/library/data/string.lean @@ -1,6 +1,11 @@ --- Copyright (c) 2014 Microsoft Corporation. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Leonardo de Moura +/- +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: data.string +Author: Leonardo de Moura +-/ + import data.bool open bool inhabited diff --git a/library/data/string/default.lean b/library/data/string/default.lean deleted file mode 100644 index 081e1feb2..000000000 --- a/library/data/string/default.lean +++ /dev/null @@ -1,4 +0,0 @@ --- Copyright (c) 2014 Microsoft Corporation. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Leonardo de Moura -import data.string.thms diff --git a/library/data/unit.lean b/library/data/unit.lean new file mode 100644 index 000000000..1ff796278 --- /dev/null +++ b/library/data/unit.lean @@ -0,0 +1,28 @@ +/- +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: data.unit +Author: Leonardo de Moura +-/ + +import logic.eq logic.subsingleton + +namespace unit + notation `⋆` := star + + protected theorem equal (a b : unit) : a = b := + rec_on a (rec_on b rfl) + + theorem eq_star (a : unit) : a = star := + equal a star + + protected theorem subsingleton [instance] : subsingleton unit := + subsingleton.intro (λ a b, equal a b) + + protected definition is_inhabited [instance] : inhabited unit := + inhabited.mk unit.star + + protected definition has_decidable_eq [instance] : decidable_eq unit := + take (a b : unit), decidable.inl (equal a b) +end unit diff --git a/library/data/unit/default.lean b/library/data/unit/default.lean deleted file mode 100644 index 5c8eace3d..000000000 --- a/library/data/unit/default.lean +++ /dev/null @@ -1,7 +0,0 @@ --- Copyright (c) 2014 Microsoft Corporation. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Leonardo de Moura -import data.unit.thms data.unit.insts -namespace unit - notation `⋆` := star -end unit diff --git a/library/data/unit/insts.lean b/library/data/unit/insts.lean deleted file mode 100644 index 69704064c..000000000 --- a/library/data/unit/insts.lean +++ /dev/null @@ -1,16 +0,0 @@ --- Copyright (c) 2014 Microsoft Corporation. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Leonardo de Moura -import data.unit.thms logic.subsingleton -open decidable - -namespace unit - protected theorem subsingleton [instance] : subsingleton unit := - subsingleton.intro (λ a b, equal a b) - - protected definition is_inhabited [instance] : inhabited unit := - inhabited.mk unit.star - - protected definition has_decidable_eq [instance] : decidable_eq unit := - take (a b : unit), inl (equal a b) -end unit diff --git a/library/data/unit/thms.lean b/library/data/unit/thms.lean deleted file mode 100644 index 571668fc6..000000000 --- a/library/data/unit/thms.lean +++ /dev/null @@ -1,12 +0,0 @@ --- Copyright (c) 2014 Microsoft Corporation. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Leonardo de Moura -import logic.eq - -namespace unit - protected theorem equal (a b : unit) : a = b := - rec_on a (rec_on b rfl) - - theorem eq_star (a : unit) : a = star := - equal a star -end unit