chore: update copyrights

2026-03-17 18:34:06 +00:00 · 2024-09-24 15:08:50 +10:00
37 changed files with 47 additions and 47 deletions
--- a/src/Init/Data/BitVec.lean
+++ b/src/Init/Data/BitVec.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Data.BitVec.Basic
--- a/src/Init/Data/Nat/Bitwise.lean
+++ b/src/Init/Data/Nat/Bitwise.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Data.Nat.Bitwise.Basic
--- a/src/Init/Data/Nat/Mod.lean
+++ b/src/Init/Data/Nat/Mod.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Omega
--- a/src/Init/Omega.lean
+++ b/src/Init/Omega.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Omega.Int
--- a/src/Init/Omega/Coeffs.lean
+++ b/src/Init/Omega/Coeffs.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Omega.IntList
--- a/src/Init/Omega/Constraint.lean
+++ b/src/Init/Omega/Constraint.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Omega.LinearCombo
--- a/src/Init/Omega/Int.lean
+++ b/src/Init/Omega/Int.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Data.Int.DivMod
--- a/src/Init/Omega/IntList.lean
+++ b/src/Init/Omega/IntList.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Data.List.Zip
--- a/src/Init/Omega/LinearCombo.lean
+++ b/src/Init/Omega/LinearCombo.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Omega.Coeffs
--- a/src/Init/Omega/Logic.lean
+++ b/src/Init/Omega/Logic.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.PropLemmas
--- a/src/Lean/Elab/Tactic/FalseOrByContra.lean
+++ b/src/Lean/Elab/Tactic/FalseOrByContra.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Lean.Elab.Tactic.Basic
--- a/src/Lean/Elab/Tactic/LibrarySearch.lean
+++ b/src/Lean/Elab/Tactic/LibrarySearch.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021-2024 Gabriel Ebner and Lean FRO. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Joe Hendrix, Scott Morrison
+Authors: Gabriel Ebner, Joe Hendrix, Kim Morrison
 -/
 prelude
 import Lean.Meta.Tactic.LibrarySearch
--- a/src/Lean/Elab/Tactic/Omega.lean
+++ b/src/Lean/Elab/Tactic/Omega.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Lean.Elab.Tactic.Omega.Frontend
--- a/src/Lean/Elab/Tactic/Omega/Core.lean
+++ b/src/Lean/Elab/Tactic/Omega/Core.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Omega.Constraint
--- a/src/Lean/Elab/Tactic/Omega/Frontend.lean
+++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Lean.Elab.Tactic.Omega.Core
--- a/src/Lean/Elab/Tactic/Omega/MinNatAbs.lean
+++ b/src/Lean/Elab/Tactic/Omega/MinNatAbs.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.BinderPredicates
--- a/src/Lean/Elab/Tactic/Omega/OmegaM.lean
+++ b/src/Lean/Elab/Tactic/Omega/OmegaM.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Omega.LinearCombo
--- a/src/Lean/Elab/Tactic/Repeat.lean
+++ b/src/Lean/Elab/Tactic/Repeat.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Scott Morrison
+Authors: Mario Carneiro, Kim Morrison
 -/
 prelude
 import Lean.Meta.Tactic.Repeat
--- a/src/Lean/Elab/Tactic/Rewrites.lean
+++ b/src/Lean/Elab/Tactic/Rewrites.lean
@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2023 Scott Morrison. All rights reserved.
+Copyright (c) 2023 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Lean.Elab.Tactic.Location
--- a/src/Lean/Elab/Tactic/ShowTerm.lean
+++ b/src/Lean/Elab/Tactic/ShowTerm.lean
@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2021 Scott Morrison. All rights reserved.
+Copyright (c) 2021 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison, Mario Carneiro
+Authors: Kim Morrison, Mario Carneiro
 -/
 prelude
 import Lean.Elab.ElabRules
--- a/src/Lean/Elab/Tactic/SolveByElim.lean
+++ b/src/Lean/Elab/Tactic/SolveByElim.lean
@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2021 Scott Morrison. All rights reserved.
+Copyright (c) 2021 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison, David Renshaw
+Authors: Kim Morrison, David Renshaw
 -/
 prelude
 import Lean.Meta.Tactic.SolveByElim
--- a/src/Lean/Elab/Tactic/Symm.lean
+++ b/src/Lean/Elab/Tactic/Symm.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Siddhartha Gadgil. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Siddhartha Gadgil, Mario Carneiro, Scott Morrison
+Authors: Siddhartha Gadgil, Mario Carneiro, Kim Morrison
 -/
 prelude
 import Lean.Meta.Tactic.Symm
--- a/src/Lean/LabelAttribute.lean
+++ b/src/Lean/LabelAttribute.lean
@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2023 Scott Morrison. All rights reserved.
+Copyright (c) 2023 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Lean.ScopedEnvExtension
--- a/src/Lean/Meta/DiscrTree.lean
+++ b/src/Lean/Meta/DiscrTree.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Jannis Limperg, Scott Morrison
+Authors: Leonardo de Moura, Jannis Limperg, Kim Morrison
 -/
 prelude
 import Lean.Meta.WHNF
--- a/src/Lean/Meta/LazyDiscrTree.lean
+++ b/src/Lean/Meta/LazyDiscrTree.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joe Hendrix, Scott Morrison
+Authors: Joe Hendrix, Kim Morrison
 -/
 prelude
 import Lean.Meta.CompletionName
--- a/src/Lean/Meta/Tactic/Backtrack.lean
+++ b/src/Lean/Meta/Tactic/Backtrack.lean
@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2023 Scott Morrison. All rights reserved.
+Copyright (c) 2023 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Init.Data.List.BasicAux
--- a/src/Lean/Meta/Tactic/Generalize.lean
+++ b/src/Lean/Meta/Tactic/Generalize.lean
@@ -93,7 +93,7 @@ root `*` are considered. Matching is executed using the definitionally equality
 The `generalize` tactic employs `kabstract` and defaults to standard reducibility.
 Hence, the `isDefEq` operations invoked by `kabstract` can become highly resource-intensive
 and potentially trigger "max recursion depth reached" errors, as observed in issue #3524.
-This issue was isolated by @**Scott Morrison** with the following example:
+This issue was isolated by @**Kim Morrison** with the following example:
 ```
 example (a : Nat) : ((2 ^ 7) + a) - 2 ^ 7 = 0 := by
  generalize 0 - 0 = x
--- a/src/Lean/Meta/Tactic/LibrarySearch.lean
+++ b/src/Lean/Meta/Tactic/LibrarySearch.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021-2023 Gabriel Ebner and Lean FRO. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Joe Hendrix, Scott Morrison
+Authors: Gabriel Ebner, Joe Hendrix, Kim Morrison
 -/
 prelude
 import Init.Data.Nat.MinMax
--- a/src/Lean/Meta/Tactic/Repeat.lean
+++ b/src/Lean/Meta/Tactic/Repeat.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Scott Morrison
+Authors: Mario Carneiro, Kim Morrison
 -/
 prelude
 import Lean.Meta.Basic
--- a/src/Lean/Meta/Tactic/Rewrites.lean
+++ b/src/Lean/Meta/Tactic/Rewrites.lean
@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2023 Scott Morrison. All rights reserved.
+Copyright (c) 2023 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Lean.Meta.LazyDiscrTree
--- a/src/Lean/Meta/Tactic/SolveByElim.lean
+++ b/src/Lean/Meta/Tactic/SolveByElim.lean
@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2021 Scott Morrison. All rights reserved.
+Copyright (c) 2021 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison, David Renshaw
+Authors: Kim Morrison, David Renshaw
 -/
 prelude
 import Init.Data.Sum
--- a/src/Lean/Meta/Tactic/Symm.lean
+++ b/src/Lean/Meta/Tactic/Symm.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Siddhartha Gadgil. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Siddhartha Gadgil, Mario Carneiro, Scott Morrison
+Authors: Siddhartha Gadgil, Mario Carneiro, Kim Morrison
 -/
 prelude
 import Lean.Meta.Reduce
--- a/src/Lean/Replay.lean
+++ b/src/Lean/Replay.lean
@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2023 Scott Morrison. All rights reserved.
+Copyright (c) 2023 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Lean.CoreM
--- a/src/Lean/Util/TestExtern.lean
+++ b/src/Lean/Util/TestExtern.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Lean.Elab.SyntheticMVars
--- a/tests/lean/run/match_expr_perf.lean
+++ b/tests/lean/run/match_expr_perf.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 prelude
 import Lean.Elab.Tactic.Omega.Core
--- a/tests/lean/run/show_term.lean
+++ b/tests/lean/run/show_term.lean
@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2021 Scott Morrison. All rights reserved.
+Copyright (c) 2021 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/

 /-- info: Try this: exact (n, 37) -/
--- a/tests/lean/run/solve_by_elim.lean
+++ b/tests/lean/run/solve_by_elim.lean
@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2021 Scott Morrison. All rights reserved.
+Copyright (c) 2021 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/

 import Lean.Meta.Tactic.Constructor