refactor(library): clean up headers and markdown files

This commit is contained in:
Jeremy Avigad 2014-12-22 15:33:29 -05:00
parent fe424add26
commit 6ad091d7bf
23 changed files with 163 additions and 79 deletions

View file

@ -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

View file

@ -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

View file

@ -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

View file

@ -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

View file

@ -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

View file

@ -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

View file

@ -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

View file

@ -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

View file

@ -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

View file

@ -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
Module: classical
Author: Jeremy Avigad
The standard library together with the classical axioms.
-/
import standard logic.axioms

View file

@ -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

View file

@ -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

View file

@ -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)
* [set](set.lean)
* [vector](vector.lean)

View file

@ -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

View file

@ -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

View file

@ -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

View file

@ -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

View file

@ -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

View file

@ -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

View file

@ -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)

View file

@ -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.
See also the `hott` library, a library for homotopy type theory based on a predicative
foundation.

View file

@ -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
-/

View file

@ -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