chore(*): normalise copyright headers (#4497)

This diff makes sure that all files start with a copyright header of the following shape ``` /- Copyright ... ... Apache ... Author... -/ ``` Some files used to have a short description of the contents in the same comment block. Such comments have *not* been turned into module docstrings, but simply moved to a regular comment block below the copyright header. Turning these comments into good module docstrings is an effort that should be undertaken in future PRs.
leanprover-community · Oct 7, 2020 · ed9ef1b · ed9ef1b
1 parent 3c75527
commit ed9ef1b
Show file tree

Hide file tree

Showing 27 changed files with 145 additions and 45 deletions.
diff --git a/src/data/polynomial/field_division.lean b/src/data/polynomial/field_division.lean
@@ -1,4 +1,3 @@
-
 /-
 Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.

diff --git a/src/data/polynomial/integral_normalization.lean b/src/data/polynomial/integral_normalization.lean
@@ -1,4 +1,3 @@
-
 /-
 Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.

diff --git a/src/data/set/function.lean b/src/data/set/function.lean
@@ -1,4 +1,4 @@
-  /-
+/-
 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Jeremy Avigad, Andrew Zipperer, Haitao Zhang, Minchao Wu, Yury Kudryashov

diff --git a/src/measure_theory/category/Meas.lean b/src/measure_theory/category/Meas.lean
@@ -1,4 +1,5 @@
-/- Copyright (c) 2018 Johannes Hölzl. All rights reserved.
+/-
+Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/

diff --git a/src/tactic/derive_fintype.lean b/src/tactic/derive_fintype.lean
@@ -1,6 +1,7 @@
 /-
 Copyright (c) 2020 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
 -/
 import logic.basic
 import data.fintype.basic

diff --git a/src/tactic/derive_inhabited.lean b/src/tactic/derive_inhabited.lean
@@ -1,6 +1,7 @@
 /-
 Copyright (c) 2020 Gabriel Ebner. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner
 -/
 import logic.basic
 

diff --git a/src/tactic/interactive.lean b/src/tactic/interactive.lean
@@ -1,4 +1,3 @@
-
 /-
 Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.

diff --git a/src/tactic/omega/clause.lean b/src/tactic/omega/clause.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Definition of linear constrain clauses.
+-/
 
-Definition of linear constrain clauses. -/
 import tactic.omega.term
 
 namespace omega

diff --git a/src/tactic/omega/coeffs.lean b/src/tactic/omega/coeffs.lean
@@ -1,9 +1,14 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
 
+/-
 Non-constant terms of linear constraints are represented
-by storing their coefficients in integer lists. -/
+by storing their coefficients in integer lists.
+-/
+
 import data.list.func
 import tactic.ring
 import tactic.omega.misc

diff --git a/src/tactic/omega/eq_elim.lean b/src/tactic/omega/eq_elim.lean
@@ -1,9 +1,14 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
 
+/-
 Correctness lemmas for equality elimination.
-See 5.5 of <http://www.decision-procedures.org/> for details. -/
+See 5.5 of <http://www.decision-procedures.org/> for details.
+-/
+
 import tactic.omega.clause
 
 open list.func

diff --git a/src/tactic/omega/find_ees.lean b/src/tactic/omega/find_ees.lean
@@ -1,9 +1,14 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
 
+/-
 A tactic for finding a sequence of equality
-elimination rules for a given set of constraints. -/
+elimination rules for a given set of constraints.
+-/
+
 import tactic.omega.eq_elim
 
 variables {α β : Type}

diff --git a/src/tactic/omega/find_scalars.lean b/src/tactic/omega/find_scalars.lean
@@ -1,9 +1,14 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
 
+/-
 Tactic for performing Fourier–Motzkin elimination to find
-a contradictory linear combination of input constraints. -/
+a contradictory linear combination of input constraints.
+-/
+
 import tactic.omega.term
 import data.list.min_max
 

diff --git a/src/tactic/omega/int/dnf.lean b/src/tactic/omega/int/dnf.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+DNF transformation.
+-/
 
-DNF transformation. -/
 import tactic.omega.clause
 import tactic.omega.int.form
 

diff --git a/src/tactic/omega/int/form.lean b/src/tactic/omega/int/form.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Linear integer arithmetic formulas in pre-normalized form.
+-/
 
-Linear integer arithmetic formulas in pre-normalized form. -/
 import tactic.omega.int.preterm
 
 namespace omega

diff --git a/src/tactic/omega/int/main.lean b/src/tactic/omega/int/main.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Main procedure for linear integer arithmetic.
+-/
 
-Main procedure for linear integer arithmetic. -/
 import tactic.omega.prove_unsats
 import tactic.omega.int.dnf
 

diff --git a/src/tactic/omega/int/preterm.lean b/src/tactic/omega/int/preterm.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Linear integer arithmetic terms in pre-normalized form.
+-/
 
-Linear integer arithmetic terms in pre-normalized form. -/
 import tactic.omega.term
 
 namespace omega

diff --git a/src/tactic/omega/lin_comb.lean b/src/tactic/omega/lin_comb.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Linear combination of constraints.
+-/
 
-Linear combination of constraints. -/
 import tactic.omega.clause
 
 namespace omega

diff --git a/src/tactic/omega/main.lean b/src/tactic/omega/main.lean
@@ -1,9 +1,14 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
 
+/-
 A tactic for discharging linear integer & natural
-number arithmetic goals using the Omega test. -/
+number arithmetic goals using the Omega test.
+-/
+
 import tactic.omega.int.main
 import tactic.omega.nat.main
 

diff --git a/src/tactic/omega/misc.lean b/src/tactic/omega/misc.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Miscellaneous.
+-/
 
-Miscellaneous. -/
 import tactic.localized
 
 variables {α β γ : Type}

diff --git a/src/tactic/omega/nat/dnf.lean b/src/tactic/omega/nat/dnf.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+DNF transformation.
+-/
 
-DNF transformation. -/
 import tactic.omega.clause
 import tactic.omega.nat.form
 

diff --git a/src/tactic/omega/nat/form.lean b/src/tactic/omega/nat/form.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Linear natural number arithmetic preformulas in pre-normalized preform.
+-/
 
-Linear natural number arithmetic preformulas in pre-normalized preform. -/
 import tactic.omega.nat.preterm
 
 namespace omega

diff --git a/src/tactic/omega/nat/main.lean b/src/tactic/omega/nat/main.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Main procedure for linear natural number arithmetic.
+-/
 
-Main procedure for linear natural number arithmetic. -/
 import tactic.omega.prove_unsats
 import tactic.omega.nat.dnf
 import tactic.omega.nat.neg_elim

diff --git a/src/tactic/omega/nat/neg_elim.lean b/src/tactic/omega/nat/neg_elim.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Negation elimination.
+-/
 
-Negation elimination. -/
 import tactic.omega.nat.form
 
 namespace omega

diff --git a/src/tactic/omega/nat/preterm.lean b/src/tactic/omega/nat/preterm.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Linear natural number arithmetic terms in pre-normalized form.
+-/
 
-Linear natural number arithmetic terms in pre-normalized form. -/
 import tactic.omega.term
 
 open tactic

diff --git a/src/tactic/omega/nat/sub_elim.lean b/src/tactic/omega/nat/sub_elim.lean
@@ -1,10 +1,15 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
 
+/-
 Subtraction elimination for linear natural number arithmetic.
 Works by repeatedly rewriting goals of the preform `P[t-s]` into
-`P[x] ∧ (t = s + x ∨ (t ≤ s ∧ x = 0))`, where `x` is fresh. -/
+`P[x] ∧ (t = s + x ∨ (t ≤ s ∧ x = 0))`, where `x` is fresh.
+-/
+
 import tactic.omega.nat.form
 
 namespace omega

diff --git a/src/tactic/omega/prove_unsats.lean b/src/tactic/omega/prove_unsats.lean
@@ -1,9 +1,14 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
 
+/-
 A tactic which constructs exprs to discharge
-goals of the form `clauses.unsat cs`. -/
+goals of the form `clauses.unsat cs`.
+-/
+
 import tactic.omega.find_ees
 import tactic.omega.find_scalars
 import tactic.omega.lin_comb

diff --git a/src/tactic/omega/term.lean b/src/tactic/omega/term.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Normalized linear integer arithmetic terms.
+-/
 
-Normalized linear integer arithmetic terms. -/
 import tactic.omega.coeffs
 
 namespace omega