Add copyright

Linyxus · Linyxus · commit 25f0d6263737 · 2025-09-13T23:47:34.000+02:00
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
 /-
 # Intrinsically scoped de Bruijn indices
 
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Eval.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Eval.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
 /-
 # Big-step evaluator for System F<:
 -/
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
 /-
 # Rebinding morphisms
 
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
 import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RebindTheory.Core
 import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSystem
 import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Properties
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
 /-
 # Operational semantics for System F<:
 
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
 /-
 # Retyping morphisms
 
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
 import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.Core
 
 /-- Context retyping preserves subtyping judgments. -/
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
 /-
 # Parallel substitution for System F<:
 
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
 /-
 # Parallel substitution for System F<:
 
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
 /-
 # Properties of parallel substitution for System F<:
 
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
 /-
 # System F<: syntax
 
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
 /-
 # Typing contexts for System F<:
 
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
 /-
 # Core syntax for System F<:
 
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
 /-
 # Substitution operations for System F<: syntax
 
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
 /-
 # Canonical forms lemmas for System F<:
 -/
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
 /-
 # Preservation theorem for System F<:
 
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Progress.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Progress.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
 /-
 # Progress theorem for System F<:
 
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
 /-
 # Type system for System F<:
 
