From 8bebd104ff0739396cf68f2f6e52b6ae454e399f Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sat, 23 May 2015 20:52:23 +1000 Subject: [PATCH] refactor(library/*): remove 'Module:' lines --- library/algebra/binary.lean | 2 -- library/algebra/bundled.lean | 2 -- library/algebra/category/adjoint.lean | 2 -- library/algebra/category/basic.lean | 2 -- library/algebra/category/default.lean | 2 -- library/algebra/category/functor.lean | 2 -- library/algebra/category/limit.lean | 2 -- library/algebra/category/morphism.lean | 2 -- library/algebra/category/natural_transformation.lean | 2 -- library/algebra/category/yoneda.lean | 2 -- library/algebra/field.lean | 2 -- library/algebra/function.lean | 2 -- library/algebra/order.lean | 2 -- library/algebra/ordered_field.lean | 2 -- library/algebra/ordered_group.lean | 2 -- library/algebra/ordered_ring.lean | 2 -- library/algebra/relation.lean | 2 -- library/algebra/ring.lean | 2 -- library/classical.lean | 2 -- library/data/bool.lean | 2 -- library/data/countable.lean | 2 -- library/data/empty.lean | 2 -- library/data/encodable.lean | 2 -- library/data/examples/depchoice.lean | 2 -- library/data/examples/notencodable.lean | 2 -- library/data/fin.lean | 2 -- library/data/int/default.lean | 2 -- library/data/int/div.lean | 2 -- library/data/list/as_type.lean | 2 -- library/data/list/basic.lean | 2 -- library/data/nat/bquant.lean | 2 -- library/data/nat/choose.lean | 2 -- library/data/nat/div.lean | 2 -- library/data/nat/pairing.lean | 2 -- library/data/nat/sqrt.lean | 2 -- library/data/nat/sub.lean | 2 -- library/data/num.lean | 2 -- library/data/option.lean | 2 -- library/data/prod.lean | 2 -- library/data/rat/basic.lean | 2 -- library/data/rat/order.lean | 2 -- library/data/set/classical_inverse.lean | 2 -- library/data/set/default.lean | 2 -- library/data/set/function.lean | 2 -- library/data/set/map.lean | 2 -- library/data/sigma.lean | 2 -- library/data/squash.lean | 2 -- library/data/stream.lean | 2 -- library/data/string.lean | 2 -- library/data/subtype.lean | 2 -- library/data/sum.lean | 2 -- library/data/unit.lean | 2 -- library/data/uprod.lean | 2 -- library/data/vector.lean | 2 -- library/init/datatypes.lean | 2 -- library/init/default.lean | 2 -- library/init/funext.lean | 2 -- library/init/logic.lean | 2 -- library/init/measurable.lean | 2 -- library/init/nat.lean | 2 -- library/init/num.lean | 2 -- library/init/priority.lean | 2 -- library/init/prod.lean | 2 -- library/init/quot.lean | 2 -- library/init/reserved_notation.lean | 2 -- library/init/sigma.lean | 2 -- library/init/tactic.lean | 2 -- library/init/wf.lean | 2 -- library/logic/axioms/classical.lean | 2 -- library/logic/axioms/em.lean | 2 -- library/logic/axioms/hilbert.lean | 2 -- library/logic/axioms/prop_complete.lean | 2 -- library/logic/axioms/prop_decidable.lean | 2 -- library/logic/cast.lean | 2 -- library/logic/default.lean | 2 -- library/logic/eq.lean | 2 -- library/logic/examples/instances_test.lean | 2 -- library/logic/identities.lean | 2 -- library/logic/instances.lean | 2 -- library/logic/quantifiers.lean | 2 -- library/standard.lean | 2 -- tests/lean/run/finbug.lean | 2 -- tests/lean/run/finbug2.lean | 2 -- 83 files changed, 166 deletions(-) diff --git a/library/algebra/binary.lean b/library/algebra/binary.lean index 078e25cb0..1af950118 100644 --- a/library/algebra/binary.lean +++ b/library/algebra/binary.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.binary Authors: Leonardo de Moura, Jeremy Avigad General properties of binary operations. diff --git a/library/algebra/bundled.lean b/library/algebra/bundled.lean index ea41110d5..94efaa25f 100644 --- a/library/algebra/bundled.lean +++ b/library/algebra/bundled.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.bundled Authors: Jeremy Avigad Bundled structures diff --git a/library/algebra/category/adjoint.lean b/library/algebra/category/adjoint.lean index bb41d6014..88c7bf067 100644 --- a/library/algebra/category/adjoint.lean +++ b/library/algebra/category/adjoint.lean @@ -1,8 +1,6 @@ /- 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 -/ diff --git a/library/algebra/category/basic.lean b/library/algebra/category/basic.lean index c165a8a67..d2176572d 100644 --- a/library/algebra/category/basic.lean +++ b/library/algebra/category/basic.lean @@ -1,8 +1,6 @@ /- 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 -/ open eq eq.ops diff --git a/library/algebra/category/default.lean b/library/algebra/category/default.lean index e5656b3ed..7c35a9c4e 100644 --- a/library/algebra/category/default.lean +++ b/library/algebra/category/default.lean @@ -1,8 +1,6 @@ /- 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 -/ diff --git a/library/algebra/category/functor.lean b/library/algebra/category/functor.lean index 580f18ae8..d07f9f33a 100644 --- a/library/algebra/category/functor.lean +++ b/library/algebra/category/functor.lean @@ -1,8 +1,6 @@ /- 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 diff --git a/library/algebra/category/limit.lean b/library/algebra/category/limit.lean index 41c726f22..1ac6aea04 100644 --- a/library/algebra/category/limit.lean +++ b/library/algebra/category/limit.lean @@ -1,8 +1,6 @@ /- 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 -/ diff --git a/library/algebra/category/morphism.lean b/library/algebra/category/morphism.lean index a1f8616a3..97ffc91e0 100644 --- a/library/algebra/category/morphism.lean +++ b/library/algebra/category/morphism.lean @@ -1,8 +1,6 @@ /- 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 -/ diff --git a/library/algebra/category/natural_transformation.lean b/library/algebra/category/natural_transformation.lean index 184e4732b..1357b3a56 100644 --- a/library/algebra/category/natural_transformation.lean +++ b/library/algebra/category/natural_transformation.lean @@ -1,8 +1,6 @@ /- 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 -/ diff --git a/library/algebra/category/yoneda.lean b/library/algebra/category/yoneda.lean index 7d1983b08..75f0c7f35 100644 --- a/library/algebra/category/yoneda.lean +++ b/library/algebra/category/yoneda.lean @@ -1,8 +1,6 @@ /- 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 -/ diff --git a/library/algebra/field.lean b/library/algebra/field.lean index 6fa18d27c..2f8e441d1 100644 --- a/library/algebra/field.lean +++ b/library/algebra/field.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Robert Lewis. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.field Authors: Robert Lewis Structures with multiplicative and additive components, including division rings and fields. diff --git a/library/algebra/function.lean b/library/algebra/function.lean index c7ef29668..62a64d6ea 100644 --- a/library/algebra/function.lean +++ b/library/algebra/function.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.function Author: Leonardo de Moura General operations on functions. diff --git a/library/algebra/order.lean b/library/algebra/order.lean index b57b69d55..891e35e74 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.order Author: Jeremy Avigad Various types of orders. We develop weak orders "≤" and strict orders "<" separately. We also diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean index 8186fdd5d..dd212a40c 100644 --- a/library/algebra/ordered_field.lean +++ b/library/algebra/ordered_field.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Robert Lewis. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.ordered_field Authors: Robert Lewis -/ diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean index 015dc583c..e90de0994 100644 --- a/library/algebra/ordered_group.lean +++ b/library/algebra/ordered_group.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.ordered_group Authors: Jeremy Avigad Partially ordered additive groups, modeled on Isabelle's library. We could refine the structures, diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean index a0e1cc12a..916449d2b 100644 --- a/library/algebra/ordered_ring.lean +++ b/library/algebra/ordered_ring.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.ordered_ring Authors: Jeremy Avigad Here an "ordered_ring" is partially ordered ring, which is ordered with respect to both a weak diff --git a/library/algebra/relation.lean b/library/algebra/relation.lean index 3582439c8..e30160483 100644 --- a/library/algebra/relation.lean +++ b/library/algebra/relation.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.relation Author: Jeremy Avigad General properties of relations, and classes for equivalence relations and congruences. diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 30d73d14d..0bd34368b 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.ring Authors: Jeremy Avigad, Leonardo de Moura Structures with multiplicative and additive components, including semirings, rings, and fields. diff --git a/library/classical.lean b/library/classical.lean index a0b1c7478..fb497f98f 100644 --- a/library/classical.lean +++ b/library/classical.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: classical Author: Jeremy Avigad The standard library together with the classical axioms. diff --git a/library/data/bool.lean b/library/data/bool.lean index e4ed2e71c..5240abfe7 100644 --- a/library/data/bool.lean +++ b/library/data/bool.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.bool Author: Leonardo de Moura -/ diff --git a/library/data/countable.lean b/library/data/countable.lean index dda63c468..2f1a330ef 100644 --- a/library/data/countable.lean +++ b/library/data/countable.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.countable Author: Leonardo de Moura Define countable types diff --git a/library/data/empty.lean b/library/data/empty.lean index 7f5eb70fc..0ed1583e2 100644 --- a/library/data/empty.lean +++ b/library/data/empty.lean @@ -1,8 +1,6 @@ /- 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 -/ import logic.cast diff --git a/library/data/encodable.lean b/library/data/encodable.lean index 706bdd40b..0c2bafc0a 100644 --- a/library/data/encodable.lean +++ b/library/data/encodable.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.encodable Author: Leonardo de Moura Type class for encodable types. diff --git a/library/data/examples/depchoice.lean b/library/data/examples/depchoice.lean index f961cc24e..83afb8eeb 100644 --- a/library/data/examples/depchoice.lean +++ b/library/data/examples/depchoice.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.examples.depchoice Author: Leonardo de Moura -/ import data.encodable diff --git a/library/data/examples/notencodable.lean b/library/data/examples/notencodable.lean index e1397f5cc..c75142084 100644 --- a/library/data/examples/notencodable.lean +++ b/library/data/examples/notencodable.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.examples.unencodable Author: Leonardo de Moura Small example showing that (nat → nat) is not encodable. diff --git a/library/data/fin.lean b/library/data/fin.lean index 48fb2fbd9..0858447d7 100644 --- a/library/data/fin.lean +++ b/library/data/fin.lean @@ -1,8 +1,6 @@ /- 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. diff --git a/library/data/int/default.lean b/library/data/int/default.lean index be7f58b17..19b0463ac 100644 --- a/library/data/int/default.lean +++ b/library/data/int/default.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.int.default Author: Jeremy Avigad -/ import .basic .order .div .power diff --git a/library/data/int/div.lean b/library/data/int/div.lean index 112a6b83c..386f6023e 100644 --- a/library/data/int/div.lean +++ b/library/data/int/div.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.int.div Author: Jeremy Avigad Definitions and properties of div, mod, gcd, lcm, coprime, following the SSReflect library. diff --git a/library/data/list/as_type.lean b/library/data/list/as_type.lean index 83ec2cc58..9fc80f3b1 100644 --- a/library/data/list/as_type.lean +++ b/library/data/list/as_type.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Leonardo de Moura. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.list.as_type Authors: Leonardo de Moura -/ import data.list.basic diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index dc9fcc9ae..5f21a439d 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Parikshit Khanna. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.list.basic Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura Basic properties of lists. diff --git a/library/data/nat/bquant.lean b/library/data/nat/bquant.lean index 6bc962da2..2e3ff1ff3 100644 --- a/library/data/nat/bquant.lean +++ b/library/data/nat/bquant.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.nat.bquant Author: Leonardo de Moura Show that "bounded" quantifiers: (∃x, x < n ∧ P x) and (∀x, x < n → P x) diff --git a/library/data/nat/choose.lean b/library/data/nat/choose.lean index b8d9a4952..9b86fed3a 100644 --- a/library/data/nat/choose.lean +++ b/library/data/nat/choose.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.nat.choose Authors: Leonardo de Moura Choice function for decidable predicates on natural numbers. diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index 14922c74d..00d057e65 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.nat.div Authors: Jeremy Avigad, Leonardo de Moura Definitions and properties of div, mod, gcd, lcm, coprime. Much of the development follows diff --git a/library/data/nat/pairing.lean b/library/data/nat/pairing.lean index 369a753f2..4a3356467 100644 --- a/library/data/nat/pairing.lean +++ b/library/data/nat/pairing.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.nat.pairing Authors: Leonardo de Moura Elegant pairing function. diff --git a/library/data/nat/sqrt.lean b/library/data/nat/sqrt.lean index c051e773a..295ebda8f 100644 --- a/library/data/nat/sqrt.lean +++ b/library/data/nat/sqrt.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.nat.sqrt Authors: Leonardo de Moura Very simple (sqrt n) function that returns s s.t. diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean index 2b3a67df9..fa5c3d8b5 100644 --- a/library/data/nat/sub.lean +++ b/library/data/nat/sub.lean @@ -3,8 +3,6 @@ Copyright (c) 2014 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn, Jeremy Avigad -Module: data.nat.sub - Subtraction on the natural numbers, as well as min, max, and distance. -/ import .order diff --git a/library/data/num.lean b/library/data/num.lean index 0662e05f7..758d95c8b 100644 --- a/library/data/num.lean +++ b/library/data/num.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.num Author: Leonardo de Moura -/ import data.bool tools.helper_tactics diff --git a/library/data/option.lean b/library/data/option.lean index 1aada7052..bf15efd78 100644 --- a/library/data/option.lean +++ b/library/data/option.lean @@ -1,8 +1,6 @@ /- 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 -/ diff --git a/library/data/prod.lean b/library/data/prod.lean index 7daf6ad47..1e0198029 100644 --- a/library/data/prod.lean +++ b/library/data/prod.lean @@ -1,8 +1,6 @@ /- 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 diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean index d0982cd8f..3c0966de7 100644 --- a/library/data/rat/basic.lean +++ b/library/data/rat/basic.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.rat.basic Author: Jeremy Avigad The rational numbers as a field generated by the integers, defined as the usual quotient. diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean index b0e39f5f2..e43ab8af8 100644 --- a/library/data/rat/order.lean +++ b/library/data/rat/order.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.rat.order Author: Jeremy Avigad Adds the ordering, and instantiates the rationals as an ordered field. diff --git a/library/data/set/classical_inverse.lean b/library/data/set/classical_inverse.lean index ac1d6b4db..37f350a46 100644 --- a/library/data/set/classical_inverse.lean +++ b/library/data/set/classical_inverse.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.set.function Author: Jeremy Avigad, Andrew Zipperer Using classical logic, defines an inverse function. diff --git a/library/data/set/default.lean b/library/data/set/default.lean index 600339d23..b10e1aead 100644 --- a/library/data/set/default.lean +++ b/library/data/set/default.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.set.default Author: Jeremy Avigad -/ import .basic .function .map diff --git a/library/data/set/function.lean b/library/data/set/function.lean index 0ee35ec5d..53d7c12f2 100644 --- a/library/data/set/function.lean +++ b/library/data/set/function.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.set.function Author: Jeremy Avigad, Andrew Zipperer, Haitao Zhang Functions between subsets of finite types. diff --git a/library/data/set/map.lean b/library/data/set/map.lean index 2a1878004..52de59ebd 100644 --- a/library/data/set/map.lean +++ b/library/data/set/map.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.set.map Author: Jeremy Avigad, Andrew Zipperer Functions between subsets of finite types, bundled with the domain and range. diff --git a/library/data/sigma.lean b/library/data/sigma.lean index 98fb47c2e..5658e1e54 100644 --- a/library/data/sigma.lean +++ b/library/data/sigma.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.sigma Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn Sigma types, aka dependent sum. diff --git a/library/data/squash.lean b/library/data/squash.lean index 2ef9b48cb..c13c72c05 100644 --- a/library/data/squash.lean +++ b/library/data/squash.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.squash Author: Leonardo de Moura Define squash type (aka propositional truncation) using quotients. diff --git a/library/data/stream.lean b/library/data/stream.lean index 15fc2016a..46ab07e44 100644 --- a/library/data/stream.lean +++ b/library/data/stream.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.stream Author: Leonardo de Moura -/ import data.nat diff --git a/library/data/string.lean b/library/data/string.lean index 49971a69d..5efce9b5a 100644 --- a/library/data/string.lean +++ b/library/data/string.lean @@ -1,8 +1,6 @@ /- 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 diff --git a/library/data/subtype.lean b/library/data/subtype.lean index a97f4b52e..6aa894fb4 100644 --- a/library/data/subtype.lean +++ b/library/data/subtype.lean @@ -1,8 +1,6 @@ /- 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 -/ diff --git a/library/data/sum.lean b/library/data/sum.lean index ed0fe4973..10d3d9948 100644 --- a/library/data/sum.lean +++ b/library/data/sum.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.sum Authors: Leonardo de Moura, Jeremy Avigad The sum type, aka disjoint union. diff --git a/library/data/unit.lean b/library/data/unit.lean index b48be9e2e..4d340112b 100644 --- a/library/data/unit.lean +++ b/library/data/unit.lean @@ -1,8 +1,6 @@ /- 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 diff --git a/library/data/uprod.lean b/library/data/uprod.lean index ee46b9f7c..44c428218 100644 --- a/library/data/uprod.lean +++ b/library/data/uprod.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.uprod Author: Leonardo de Moura Unordered pairs diff --git a/library/data/vector.lean b/library/data/vector.lean index c3c1130b6..a46e90e0c 100644 --- a/library/data/vector.lean +++ b/library/data/vector.lean @@ -1,8 +1,6 @@ /- 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 data.list data.fin diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean index 00f7dbf12..89732ca91 100644 --- a/library/init/datatypes.lean +++ b/library/init/datatypes.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.datatypes Authors: Leonardo de Moura Basic datatypes diff --git a/library/init/default.lean b/library/init/default.lean index 829456fbc..98a54c91e 100644 --- a/library/init/default.lean +++ b/library/init/default.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.default Authors: Leonardo de Moura -/ prelude diff --git a/library/init/funext.lean b/library/init/funext.lean index 73dc630e8..6dbbb5207 100644 --- a/library/init/funext.lean +++ b/library/init/funext.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.funext Author: Jeremy Avigad Extensional equality for functions, and a proof of function extensionality from quotients. diff --git a/library/init/logic.lean b/library/init/logic.lean index d74d6e050..022be6bd1 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.logic Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn -/ prelude diff --git a/library/init/measurable.lean b/library/init/measurable.lean index aafc2f3cd..97dab5094 100644 --- a/library/init/measurable.lean +++ b/library/init/measurable.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.measurable Authors: Leonardo de Moura Types with a nat-valued complexity measure. diff --git a/library/init/nat.lean b/library/init/nat.lean index 621df7f7d..7914bf340 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.nat Authors: Floris van Doorn, Leonardo de Moura -/ prelude diff --git a/library/init/num.lean b/library/init/num.lean index d26a84f1c..ca83897be 100644 --- a/library/init/num.lean +++ b/library/init/num.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.num Authors: Leonardo de Moura -/ diff --git a/library/init/priority.lean b/library/init/priority.lean index 705ecd779..27d671129 100644 --- a/library/init/priority.lean +++ b/library/init/priority.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.priority Authors: Leonardo de Moura -/ prelude diff --git a/library/init/prod.lean b/library/init/prod.lean index a29ec3dce..34e7ca7be 100644 --- a/library/init/prod.lean +++ b/library/init/prod.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.prod Author: Leonardo de Moura, Jeremy Avigad -/ prelude diff --git a/library/init/quot.lean b/library/init/quot.lean index dd5c4c937..5a283b47c 100644 --- a/library/init/quot.lean +++ b/library/init/quot.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.quot Author: Leonardo de Moura Quotient types. diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean index 7ed4ce1ae..b08af371c 100644 --- a/library/init/reserved_notation.lean +++ b/library/init/reserved_notation.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.reserved_notation Authors: Leonardo de Moura, Jeremy Avigad -/ prelude diff --git a/library/init/sigma.lean b/library/init/sigma.lean index fbc810a30..3a7f02601 100644 --- a/library/init/sigma.lean +++ b/library/init/sigma.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.sigma Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn -/ prelude diff --git a/library/init/tactic.lean b/library/init/tactic.lean index fe05fbf69..d8f2e70a4 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.tactic Author: Leonardo de Moura This is just a trick to embed the 'tactic language' as a Lean diff --git a/library/init/wf.lean b/library/init/wf.lean index c6abc70da..e0e101c04 100644 --- a/library/init/wf.lean +++ b/library/init/wf.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: init.wf Author: Leonardo de Moura -/ prelude diff --git a/library/logic/axioms/classical.lean b/library/logic/axioms/classical.lean index 773535444..bc834761d 100644 --- a/library/logic/axioms/classical.lean +++ b/library/logic/axioms/classical.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: logic.axioms.classical Author: Jeremy Avigad -/ import logic.axioms.prop_complete logic.axioms.hilbert diff --git a/library/logic/axioms/em.lean b/library/logic/axioms/em.lean index 4d9a67268..7b644e359 100644 --- a/library/logic/axioms/em.lean +++ b/library/logic/axioms/em.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: logic.axioms.funext Author: Leonardo de Moura Excluded middle diff --git a/library/logic/axioms/hilbert.lean b/library/logic/axioms/hilbert.lean index 893fa62f5..70eaa0aa0 100644 --- a/library/logic/axioms/hilbert.lean +++ b/library/logic/axioms/hilbert.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: logic.axioms.hilbert Authors: Leonardo de Moura, Jeremy Avigad Follows Coq.Logic.ClassicalEpsilon (but our definition of "inhabited" is the constructive one). diff --git a/library/logic/axioms/prop_complete.lean b/library/logic/axioms/prop_complete.lean index 2c1f4a7d1..2b9ef8e5c 100644 --- a/library/logic/axioms/prop_complete.lean +++ b/library/logic/axioms/prop_complete.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: logic.axioms.classical Author: Leonardo de Moura -/ import logic.connectives logic.quantifiers logic.cast algebra.relation diff --git a/library/logic/axioms/prop_decidable.lean b/library/logic/axioms/prop_decidable.lean index 14daeeb83..02e73171b 100644 --- a/library/logic/axioms/prop_decidable.lean +++ b/library/logic/axioms/prop_decidable.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: logic.axioms.prop_decidable Author: Leonardo de Moura Excluded middle + Hilbert implies every proposition is decidable. diff --git a/library/logic/cast.lean b/library/logic/cast.lean index 54d48e997..6d90638b2 100644 --- a/library/logic/cast.lean +++ b/library/logic/cast.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: cast.lean Author: Leonardo de Moura Casts and heterogeneous equality. See also init.datatypes and init.logic. diff --git a/library/logic/default.lean b/library/logic/default.lean index 8353bc33c..fc251202e 100644 --- a/library/logic/default.lean +++ b/library/logic/default.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: logic.default Author: Jeremy Avigad -/ import logic.eq logic.connectives logic.cast diff --git a/library/logic/eq.lean b/library/logic/eq.lean index a527a4c75..19570c48a 100644 --- a/library/logic/eq.lean +++ b/library/logic/eq.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: logic.eq Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn Additional declarations/theorems about equality. See also init.datatypes and init.logic. diff --git a/library/logic/examples/instances_test.lean b/library/logic/examples/instances_test.lean index 1bb7e9d59..c0181cb1f 100644 --- a/library/logic/examples/instances_test.lean +++ b/library/logic/examples/instances_test.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: logic.examples.instances_test Author: Jeremy Avigad Illustrates substitution and congruence with iff. diff --git a/library/logic/identities.lean b/library/logic/identities.lean index 799fcb96c..d94309aae 100644 --- a/library/logic/identities.lean +++ b/library/logic/identities.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: logic.identities Authors: Jeremy Avigad, Leonardo de Moura Useful logical identities. Since we are not using propositional extensionality, some of the diff --git a/library/logic/instances.lean b/library/logic/instances.lean index 42e10b7e4..e9ac41a61 100644 --- a/library/logic/instances.lean +++ b/library/logic/instances.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: logic.instances Author: Jeremy Avigad Class instances for iff and eq. diff --git a/library/logic/quantifiers.lean b/library/logic/quantifiers.lean index f9eeb3a19..357528cfc 100644 --- a/library/logic/quantifiers.lean +++ b/library/logic/quantifiers.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: logic.quantifiers Authors: Leonardo de Moura, Jeremy Avigad Universal and existential quantifiers. See also init.logic. diff --git a/library/standard.lean b/library/standard.lean index d933fa7d4..82b228ac3 100644 --- a/library/standard.lean +++ b/library/standard.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: standard Authors: Leonardo de Moura, Jeremy Avigad The constructive core of Lean's library. diff --git a/tests/lean/run/finbug.lean b/tests/lean/run/finbug.lean index 5ddec75d0..39b7cd226 100644 --- a/tests/lean/run/finbug.lean +++ b/tests/lean/run/finbug.lean @@ -1,8 +1,6 @@ /- 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. diff --git a/tests/lean/run/finbug2.lean b/tests/lean/run/finbug2.lean index 31c3a3233..bcaf3b519 100644 --- a/tests/lean/run/finbug2.lean +++ b/tests/lean/run/finbug2.lean @@ -1,8 +1,6 @@ /- 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.