From 6ad091d7bf4bdd830d156ba90a43764ded7bda3e Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Mon, 22 Dec 2014 15:33:29 -0500 Subject: [PATCH] refactor(library): clean up headers and markdown files --- library/algebra/algebra.md | 3 +++ library/algebra/category/adjoint.lean | 10 +++++++--- library/algebra/category/basic.lean | 10 +++++++--- library/algebra/category/default.lean | 10 +++++++--- library/algebra/category/functor.lean | 10 +++++++--- library/algebra/category/limit.lean | 10 +++++++--- library/algebra/category/morphism.lean | 10 +++++++--- .../category/natural_transformation.lean | 10 +++++++--- library/algebra/category/yoneda.lean | 10 +++++++--- library/classical.lean | 14 ++++++++++---- library/data/bool/default.lean | 11 ++++++++--- library/data/bool/thms.lean | 11 ++++++++--- library/data/data.md | 8 +++++--- library/data/fin.lean | 10 ++++++++++ library/data/num/default.lean | 13 ++++++++----- library/data/num/thms.lean | 13 ++++++++----- library/data/option.lean | 11 ++++++++--- library/data/set.lean | 13 ++++++++----- library/data/subtype.lean | 11 ++++++++--- library/data/vector.lean | 18 +++++++++++------- library/library.md | 11 ++++------- library/logic/axioms/classical.lean | 2 +- library/standard.lean | 13 +++++++------ 23 files changed, 163 insertions(+), 79 deletions(-) diff --git a/library/algebra/algebra.md b/library/algebra/algebra.md index b95e7492dc..10479cc7ab 100644 --- a/library/algebra/algebra.md +++ b/library/algebra/algebra.md @@ -8,5 +8,8 @@ Algebraic structures. * [binary](binary.lean) : binary operations * [wf](wf.lean) : well-founded relations * [group](group.lean) +* [ring](ring.lean) +* [ordered_group](ordered_group.lean) +* [ordered_ring](ordered_ring.lean) * [category](category/category.md) : category theory diff --git a/library/algebra/category/adjoint.lean b/library/algebra/category/adjoint.lean index 7b295500e1..bb41d6014e 100644 --- a/library/algebra/category/adjoint.lean +++ b/library/algebra/category/adjoint.lean @@ -1,6 +1,10 @@ --- Copyright (c) 2014 Floris van Doorn. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Floris van Doorn +/- +Copyright (c) 2014 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: algebra.category.adjoint +Author: Floris van Doorn +-/ import .constructions diff --git a/library/algebra/category/basic.lean b/library/algebra/category/basic.lean index a87916c433..e4818cafb4 100644 --- a/library/algebra/category/basic.lean +++ b/library/algebra/category/basic.lean @@ -1,6 +1,10 @@ --- Copyright (c) 2014 Floris van Doorn. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Floris van Doorn +/- +Copyright (c) 2014 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: algebra.category.basic +Author: Floris van Doorn +-/ import logic.axioms.funext diff --git a/library/algebra/category/default.lean b/library/algebra/category/default.lean index 7e84a0731a..e5656b3edd 100644 --- a/library/algebra/category/default.lean +++ b/library/algebra/category/default.lean @@ -1,5 +1,9 @@ --- Copyright (c) 2014 Floris van Doorn. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Floris van Doorn +/- +Copyright (c) 2014 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: algebra.category.default +Author: Floris van Doorn +-/ import .morphism .constructions diff --git a/library/algebra/category/functor.lean b/library/algebra/category/functor.lean index 8bbc7fc9b4..7257b3ffbd 100644 --- a/library/algebra/category/functor.lean +++ b/library/algebra/category/functor.lean @@ -1,6 +1,10 @@ --- Copyright (c) 2014 Floris van Doorn. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Floris van Doorn +/- +Copyright (c) 2014 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: algebra.category.functor +Author: Floris van Doorn +-/ import .basic import logic.cast diff --git a/library/algebra/category/limit.lean b/library/algebra/category/limit.lean index 79ad761193..41c726f22c 100644 --- a/library/algebra/category/limit.lean +++ b/library/algebra/category/limit.lean @@ -1,6 +1,10 @@ --- Copyright (c) 2014 Floris van Doorn. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Floris van Doorn +/- +Copyright (c) 2014 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: algebra.category.limit +Author: Floris van Doorn +-/ import .natural_transformation import data.sigma diff --git a/library/algebra/category/morphism.lean b/library/algebra/category/morphism.lean index 18bd0ac051..bb71351f41 100644 --- a/library/algebra/category/morphism.lean +++ b/library/algebra/category/morphism.lean @@ -1,6 +1,10 @@ --- Copyright (c) 2014 Floris van Doorn. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Floris van Doorn +/- +Copyright (c) 2014 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: algebra.category.morphism +Author: Floris van Doorn +-/ import .basic algebra.relation algebra.binary diff --git a/library/algebra/category/natural_transformation.lean b/library/algebra/category/natural_transformation.lean index 827ab7bf2c..dc77986552 100644 --- a/library/algebra/category/natural_transformation.lean +++ b/library/algebra/category/natural_transformation.lean @@ -1,6 +1,10 @@ --- Copyright (c) 2014 Floris van Doorn. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Floris van Doorn +/- +Copyright (c) 2014 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: algebra.category.natural_transformation +Author: Floris van Doorn +-/ import .functor open category eq eq.ops functor diff --git a/library/algebra/category/yoneda.lean b/library/algebra/category/yoneda.lean index 72176d6574..7d1983b082 100644 --- a/library/algebra/category/yoneda.lean +++ b/library/algebra/category/yoneda.lean @@ -1,6 +1,10 @@ --- Copyright (c) 2014 Floris van Doorn. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Floris van Doorn +/- +Copyright (c) 2014 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: algebra.category.yoneda +Author: Floris van Doorn +-/ import .constructions diff --git a/library/classical.lean b/library/classical.lean index 464f744fc4..b06e00ec51 100644 --- a/library/classical.lean +++ b/library/classical.lean @@ -1,5 +1,11 @@ --- Copyright (c) 2014 Jeremy Avigad. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Jeremy Avigad +/- +Copyright (c) 2014 Jeremy Avigad. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. -import standard logic.axioms \ No newline at end of file +Module: classical +Author: Jeremy Avigad + +The standard library together with the classical axioms. +-/ + +import standard logic.axioms diff --git a/library/data/bool/default.lean b/library/data/bool/default.lean index e34eb42e65..f5d1281005 100644 --- a/library/data/bool/default.lean +++ b/library/data/bool/default.lean @@ -1,4 +1,9 @@ --- 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.bool.default +Author: Leonardo de Moura +-/ + import data.bool.thms diff --git a/library/data/bool/thms.lean b/library/data/bool/thms.lean index 7b28f2609c..5b1242b313 100644 --- a/library/data/bool/thms.lean +++ b/library/data/bool/thms.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.bool.thms +Author: Leonardo de Moura +-/ + import logic.eq open eq eq.ops decidable diff --git a/library/data/data.md b/library/data/data.md index 78d1b8979f..c3cb7a132b 100644 --- a/library/data/data.md +++ b/library/data/data.md @@ -7,10 +7,11 @@ Basic types: * [empty](empty.lean) : the empty type * [unit](unit.lean) : the singleton type -* [bool](bool.lean) : the boolean values -* [num](num.lean) : generic numerals +* [bool](bool/bool.md) : the boolean values +* [num](num/num.md) : generic numerals * [string](string.lean) : ascii strings * [nat](nat/nat.md) : the natural numbers +* [fin](fin.lean) : finite ordinals * [int](int/int.md) : the integers Constructors: @@ -22,4 +23,5 @@ Constructors: * [subtype](subtype.lean) * [quotient](quotient/quotient.md) * [list](list/list.md) -* [set](set.lean) \ No newline at end of file +* [set](set.lean) +* [vector](vector.lean) \ No newline at end of file diff --git a/library/data/fin.lean b/library/data/fin.lean index cfe42f86b4..8f97336ab3 100644 --- a/library/data/fin.lean +++ b/library/data/fin.lean @@ -1,3 +1,13 @@ +/- +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: data.fin +Author: Leonardo de Moura + +Finite ordinals. +-/ + import data.nat logic.cast open nat diff --git a/library/data/num/default.lean b/library/data/num/default.lean index 2d864d935d..79e821538f 100644 --- a/library/data/num/default.lean +++ b/library/data/num/default.lean @@ -1,6 +1,9 @@ ----------------------------------------------------------------------------------------------------- --- 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.num.default +Author: Leonardo de Moura +-/ + import data.num.thms diff --git a/library/data/num/thms.lean b/library/data/num/thms.lean index 21d40d0b69..f40093bb09 100644 --- a/library/data/num/thms.lean +++ b/library/data/num/thms.lean @@ -1,8 +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.num.thms +Author: Leonardo de Moura +-/ + import logic.eq open bool diff --git a/library/data/option.lean b/library/data/option.lean index ad8bcf0eed..a2c2ddadbb 100644 --- a/library/data/option.lean +++ b/library/data/option.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.option +Author: Leonardo de Moura +-/ + import logic.eq open eq.ops decidable diff --git a/library/data/set.lean b/library/data/set.lean index 24b5226b31..5bc32c3d49 100644 --- a/library/data/set.lean +++ b/library/data/set.lean @@ -1,8 +1,11 @@ ----------------------------------------------------------------------------------------------------- ---- Copyright (c) 2014 Jeremy Avigad. All rights reserved. ---- Released under Apache 2.0 license as described in the file LICENSE. ---- Author: Jeremy Avigad, Leonardo de Moura ----------------------------------------------------------------------------------------------------- +/- +Copyright (c) 2014 Jeremy Avigad. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: data.set +Author: Jeremy Avigad, Leonardo de Moura +-/ + import data.bool open eq.ops bool diff --git a/library/data/subtype.lean b/library/data/subtype.lean index ba55a2ad3d..67967c5def 100644 --- a/library/data/subtype.lean +++ b/library/data/subtype.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.subtype +Author: Leonardo de Moura, Jeremy Avigad +-/ + open decidable set_option structure.proj_mk_thm true diff --git a/library/data/vector.lean b/library/data/vector.lean index 635fe63167..e7889d2c23 100644 --- a/library/data/vector.lean +++ b/library/data/vector.lean @@ -1,6 +1,11 @@ --- Copyright (c) 2014 Floris van Doorn. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Floris van Doorn, Leonardo de Moura +/- +Copyright (c) 2014 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: data.vector +Author: Floris van Doorn, Leonardo de Moura +-/ + import data.nat.basic data.empty data.prod open nat eq.ops prod @@ -156,8 +161,7 @@ namespace vector ... = head v :: tail v : prod.eta ... = v : vector.eta) - -- Length - -- ------ + /- Length -/ definition length (v : vector A n) := n @@ -172,8 +176,8 @@ namespace vector calc length (append v₁ v₂) = length v₁ ⊕ length v₂ : rfl ... = length v₁ + length v₂ : add_eq_addl - -- Concat - -- ------ + /- Concat -/ + definition concat (v : vector A n) (a : A) : vector A (succ n) := vector.rec_on v (a :: nil) diff --git a/library/library.md b/library/library.md index 2cb975a162..7887f6e92f 100644 --- a/library/library.md +++ b/library/library.md @@ -3,11 +3,10 @@ The Lean Library The Lean library is contained in the following modules and directories: -* [general_notation](general_notation.lean) : commonly shared notation +* [init](init/init.md) : constants and theorems needed for low-level system operations * [logic](logic/logic.md) : logical constructs and axioms * [data](data/data.md) : concrete datatypes and type constructors * [algebra](algebra/algebra.md) : algebraic structures -* [hott](hott/hott.md) : homotopy type theory * [tools](tools/tools.md) : additional tools Modules can be loaded individually, but they are also be loaded by importing the @@ -15,12 +14,11 @@ following packages: * [standard](standard.lean) : constructive logic and datatypes * [classical](classical.lean) : classical mathematics -* [hott](hott/default.lean) : homotopy type theory Lean's default logical framework is a version of the Calculus of Constructions with: * an impredicative, proof-irrelevant type `Prop` of propositions -* univerve polymorphism +* universe polymorphism * a non-cumulative hierarchy of universes, `Type 1`, `Type 2`, ... above `Prop` * inductively defined types @@ -31,6 +29,5 @@ lists, and so on. The `classical` library imports the law of the excluded middle, choice functions, and propositional extensionality. See `logic/axioms` for details. -The `hott` library is compatible with the standard library, but favors "proof -relevant" versions of the logical connectives, based on `Type` rather than -`Prop`. See `hott` for details. \ No newline at end of file +See also the `hott` library, a library for homotopy type theory based on a predicative +foundation. diff --git a/library/logic/axioms/classical.lean b/library/logic/axioms/classical.lean index 2b9e880832..64df2602b2 100644 --- a/library/logic/axioms/classical.lean +++ b/library/logic/axioms/classical.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: logic.axims.classical +Module: logic.axioms.classical Author: Leonardo de Moura -/ diff --git a/library/standard.lean b/library/standard.lean index 1e27aeb263..d933fa7d41 100644 --- a/library/standard.lean +++ b/library/standard.lean @@ -1,10 +1,11 @@ --- 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 +/- +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. --- standard --- ======== +Module: standard +Authors: Leonardo de Moura, Jeremy Avigad --- The constructive core of Lean's library. +The constructive core of Lean's library. +-/ import logic data