From 8b8e001794e6a8b481d37f24fa77bb07797682a1 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 20 Feb 2024 12:49:55 +1100 Subject: [PATCH] chore: add missing copyright headers (#3411) --- script/apply.lean | 7 ++++++- src/Init/Data/BitVec.lean | 5 +++++ src/Init/Data/Nat/Bitwise.lean | 5 +++++ src/Init/Data/Nat/Dvd.lean | 6 +++++- src/Init/Data/Nat/MinMax.lean | 5 +++++ src/Init/Omega.lean | 5 +++++ src/Lean/Data/Json/Elab.lean | 6 +++--- src/Lean/Data/Xml.lean | 5 +++++ src/Lean/Data/Xml/Basic.lean | 2 -- src/Lean/Linter.lean | 5 +++++ src/Lean/Linter/Basic.lean | 5 +++++ src/Lean/Linter/Builtin.lean | 5 +++++ src/Lean/Linter/MissingDocs.lean | 1 - src/Lean/Linter/UnusedVariables.lean | 5 +++++ src/Lean/Linter/Util.lean | 5 +++++ src/Lean/Util/TestExtern.lean | 5 +++++ src/Lean/Widget/Basic.lean | 5 +++++ src/Leanc.lean | 5 +++++ src/lake/Lake/Config/LeanConfig.lean | 4 ++-- src/lake/lakefile.lean | 5 +++++ 20 files changed, 86 insertions(+), 10 deletions(-) diff --git a/script/apply.lean b/script/apply.lean index 70bf754cde..7ef01f106d 100644 --- a/script/apply.lean +++ b/script/apply.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2022 Sebastian Ullrich. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Ullrich +-/ import Lean.Runtime abbrev M := ReaderT IO.FS.Stream IO @@ -16,7 +21,7 @@ def mkTypedefFn (i : Nat) : M Unit := do emit s!"typedef obj* (*fn{i})({args}); // NOLINT\n" emit s!"#define FN{i}(f) reinterpret_cast(lean_closure_fun(f))\n" -def genSeq (n : Nat) (f : Nat → String) (sep := ", ") : String := +def genSeq (n : Nat) (f : Nat → String) (sep := ", ") : String := List.range n |>.map f |>.intersperse sep |> .join -- make string: "obj* a1, obj* a2, ..., obj* an" diff --git a/src/Init/Data/BitVec.lean b/src/Init/Data/BitVec.lean index 76049b62d3..f3fbce34a2 100644 --- a/src/Init/Data/BitVec.lean +++ b/src/Init/Data/BitVec.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ prelude import Init.Data.BitVec.Basic import Init.Data.BitVec.Bitblast diff --git a/src/Init/Data/Nat/Bitwise.lean b/src/Init/Data/Nat/Bitwise.lean index 5827803a53..2aa3a4be40 100644 --- a/src/Init/Data/Nat/Bitwise.lean +++ b/src/Init/Data/Nat/Bitwise.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ prelude import Init.Data.Nat.Bitwise.Basic import Init.Data.Nat.Bitwise.Lemmas diff --git a/src/Init/Data/Nat/Dvd.lean b/src/Init/Data/Nat/Dvd.lean index b6507a06fd..f651f305fe 100644 --- a/src/Init/Data/Nat/Dvd.lean +++ b/src/Init/Data/Nat/Dvd.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro +-/ prelude import Init.Data.Nat.Div @@ -85,7 +90,6 @@ theorem emod_pos_of_not_dvd {a b : Nat} (h : ¬ a ∣ b) : 0 < b % a := by rw [dvd_iff_mod_eq_zero] at h exact Nat.pos_of_ne_zero h - protected theorem mul_div_cancel' {n m : Nat} (H : n ∣ m) : n * (m / n) = m := by have := mod_add_div m n rwa [mod_eq_zero_of_dvd H, Nat.zero_add] at this diff --git a/src/Init/Data/Nat/MinMax.lean b/src/Init/Data/Nat/MinMax.lean index c68fce134d..bc80a0db51 100644 --- a/src/Init/Data/Nat/MinMax.lean +++ b/src/Init/Data/Nat/MinMax.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro +-/ prelude import Init.ByCases diff --git a/src/Init/Omega.lean b/src/Init/Omega.lean index 6ecfe947d4..19cd5fe16d 100644 --- a/src/Init/Omega.lean +++ b/src/Init/Omega.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2023 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ prelude import Init.Omega.Int import Init.Omega.IntList diff --git a/src/Lean/Data/Json/Elab.lean b/src/Lean/Data/Json/Elab.lean index 957c4c7522..6c882adf46 100644 --- a/src/Lean/Data/Json/Elab.lean +++ b/src/Lean/Data/Json/Elab.lean @@ -1,7 +1,7 @@ /- - Copyright (c) 2022 E.W.Ayers. All rights reserved. - Released under Apache 2.0 license as described in the file LICENSE. - Authors: E.W.Ayers, Wojciech Nawrocki +Copyright (c) 2022 E.W.Ayers. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: E.W.Ayers, Wojciech Nawrocki -/ prelude import Lean.Data.Json.FromToJson diff --git a/src/Lean/Data/Xml.lean b/src/Lean/Data/Xml.lean index c91eb088f8..ee63449402 100644 --- a/src/Lean/Data/Xml.lean +++ b/src/Lean/Data/Xml.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2021 Daniel Fabian. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Daniel Fabian +-/ prelude import Lean.Data.Xml.Basic import Lean.Data.Xml.Parser diff --git a/src/Lean/Data/Xml/Basic.lean b/src/Lean/Data/Xml/Basic.lean index a3bc48fad6..58123b3585 100644 --- a/src/Lean/Data/Xml/Basic.lean +++ b/src/Lean/Data/Xml/Basic.lean @@ -1,4 +1,3 @@ - /- Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. @@ -38,4 +37,3 @@ private partial def cToString : Content → String end instance : ToString Element := ⟨eToString⟩ instance : ToString Content := ⟨cToString⟩ - diff --git a/src/Lean/Linter.lean b/src/Lean/Linter.lean index c0fb0aa314..5038554822 100644 --- a/src/Lean/Linter.lean +++ b/src/Lean/Linter.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2022 Lars König. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lars König +-/ prelude import Lean.Linter.Util import Lean.Linter.Builtin diff --git a/src/Lean/Linter/Basic.lean b/src/Lean/Linter/Basic.lean index 471e5297dc..2b21ad88c6 100644 --- a/src/Lean/Linter/Basic.lean +++ b/src/Lean/Linter/Basic.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2022 Lars König. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lars König +-/ prelude import Lean.Data.Options diff --git a/src/Lean/Linter/Builtin.lean b/src/Lean/Linter/Builtin.lean index 0c1fd9cca0..9b7ca2b654 100644 --- a/src/Lean/Linter/Builtin.lean +++ b/src/Lean/Linter/Builtin.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2022 Lars König. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lars König +-/ prelude import Lean.Linter.Util import Lean.Elab.Command diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean index 868cf55ee3..e9c6e97882 100644 --- a/src/Lean/Linter/MissingDocs.lean +++ b/src/Lean/Linter/MissingDocs.lean @@ -1,7 +1,6 @@ /- Copyright (c) 2022 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - Authors: Mario Carneiro -/ prelude diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean index a0518a7e6c..e489d69f85 100644 --- a/src/Lean/Linter/UnusedVariables.lean +++ b/src/Lean/Linter/UnusedVariables.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2022 Sebastian Ullrich. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Ullrich +-/ prelude import Lean.Elab.Command import Lean.Util.ForEachExpr diff --git a/src/Lean/Linter/Util.lean b/src/Lean/Linter/Util.lean index c64410d1cb..7b91ab86d0 100644 --- a/src/Lean/Linter/Util.lean +++ b/src/Lean/Linter/Util.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2022 Lars König. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lars König +-/ prelude import Lean.Data.Options import Lean.Server.InfoUtils diff --git a/src/Lean/Util/TestExtern.lean b/src/Lean/Util/TestExtern.lean index 4668c85a49..a3694b92c9 100644 --- a/src/Lean/Util/TestExtern.lean +++ b/src/Lean/Util/TestExtern.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2023 Lean FRO. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ prelude import Lean.Elab.SyntheticMVars import Lean.Elab.Command diff --git a/src/Lean/Widget/Basic.lean b/src/Lean/Widget/Basic.lean index d836816242..7eec2e4d11 100644 --- a/src/Lean/Widget/Basic.lean +++ b/src/Lean/Widget/Basic.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2022 Wojciech Nawrocki. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wojciech Nawrocki +-/ prelude import Lean.Elab.InfoTree import Lean.Message diff --git a/src/Leanc.lean b/src/Leanc.lean index c516636efa..bed468a209 100644 --- a/src/Leanc.lean +++ b/src/Leanc.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2022 Sebastian Ullrich. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Ullrich +-/ import Lean.Compiler.FFI open Lean.Compiler.FFI diff --git a/src/lake/Lake/Config/LeanConfig.lean b/src/lake/Lake/Config/LeanConfig.lean index 1e24433f7a..f1135d35a5 100644 --- a/src/lake/Lake/Config/LeanConfig.lean +++ b/src/lake/Lake/Config/LeanConfig.lean @@ -1,10 +1,10 @@ -import Lean.Util.LeanOptions - /- Copyright (c) 2022 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +import Lean.Util.LeanOptions + namespace Lake /-- diff --git a/src/lake/lakefile.lean b/src/lake/lakefile.lean index e43a7760e1..d62b665e4c 100644 --- a/src/lake/lakefile.lean +++ b/src/lake/lakefile.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2022 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ import Lake.DSL open System Lake DSL