From bbe38ddc7c2b22ec61ce47b59865579fe914cd23 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Thu, 23 Mar 2023 17:10:44 +0100 Subject: [PATCH] rename testgame to adam, part 2 --- UPDATE_LEAN.sh | 2 +- client/src/index.tsx | 2 +- package.json | 2 +- server/adam/Adam.lean | 32 ++++++------- server/adam/Adam/Levels/Contradiction.lean | 14 +++--- .../Adam/Levels/Contradiction/L01_Have.lean | 6 +-- .../Levels/Contradiction/L02_Suffices.lean | 6 +-- .../Levels/Contradiction/L03_ByContra.lean | 6 +-- .../Levels/Contradiction/L04_ByContra.lean | 6 +-- .../Levels/Contradiction/L05_Contrapose.lean | 6 +-- .../Levels/Contradiction/L06_Summary.lean | 6 +-- server/adam/Adam/Levels/Function.lean | 22 ++++----- .../Adam/Levels/Function/L01_Function.lean | 4 +- server/adam/Adam/Levels/Function/L02_Let.lean | 4 +- .../Adam/Levels/Function/L03_Piecewise.lean | 4 +- .../Adam/Levels/Function/L04_Injective.lean | 4 +- .../Adam/Levels/Function/L05_Injective.lean | 4 +- .../Adam/Levels/Function/L06_Injective.lean | 4 +- .../Adam/Levels/Function/L07_Surjective.lean | 4 +- .../Adam/Levels/Function/L08_Bijective.lean | 4 +- .../Adam/Levels/Function/L09_Inverse.lean | 4 +- .../Adam/Levels/Function/L11_Inverse.lean | 4 +- server/adam/Adam/Levels/Implication.lean | 28 +++++------ .../Adam/Levels/Implication/L01_Intro.lean | 4 +- .../Adam/Levels/Implication/L02_Revert.lean | 4 +- .../Adam/Levels/Implication/L03_Apply.lean | 4 +- .../Adam/Levels/Implication/L04_Apply.lean | 4 +- .../Adam/Levels/Implication/L05_Apply.lean | 4 +- .../adam/Adam/Levels/Implication/L06_Iff.lean | 4 +- .../adam/Adam/Levels/Implication/L07_Rw.lean | 4 +- .../adam/Adam/Levels/Implication/L08_Iff.lean | 4 +- .../adam/Adam/Levels/Implication/L09_Iff.lean | 4 +- .../Adam/Levels/Implication/L10_Apply.lean | 4 +- .../Adam/Levels/Implication/L11_ByCases.lean | 4 +- .../adam/Adam/Levels/Implication/L12_Rw.lean | 4 +- .../Adam/Levels/Implication/L13_Summary.lean | 4 +- server/adam/Adam/Levels/Induction.lean | 4 +- .../Adam/Levels/Induction/L01_Induction.lean | 4 +- server/adam/Adam/Levels/Inequality.lean | 10 ++-- .../adam/Adam/Levels/Inequality/L01_LE.lean | 4 +- .../adam/Adam/Levels/Inequality/L02_Pos.lean | 4 +- .../Adam/Levels/Inequality/L03_Linarith.lean | 4 +- .../Adam/Levels/Inequality/L04_Linarith.lean | 4 +- .../Adam/Levels/Inequality/T_Induction.lean | 4 +- server/adam/Adam/Levels/Lean.lean | 10 ++-- server/adam/Adam/Levels/Lean/L01_Type.lean | 4 +- .../adam/Adam/Levels/Lean/L02_Universe.lean | 4 +- .../Levels/Lean/L03_ImplicitArguments.lean | 6 +-- .../Levels/Lean/L04_InstanceArguments.lean | 6 +-- server/adam/Adam/Levels/LeftOvers/L09_Or.lean | 4 +- .../adam/Adam/Levels/LeftOvers/L33_Prime.lean | 4 +- .../Levels/LeftOvers/L34_ExistsUnique.lean | 4 +- .../adam/Adam/Levels/LeftOvers/Lxx_Prime.lean | 4 +- .../Adam/Levels/LeftOvers/Playground.lean | 2 +- .../Adam/Levels/LeftOvers/xx_Functions.lean | 4 +- server/adam/Adam/Levels/LinearAlgebra.lean | 46 +++++++++---------- .../Adam/Levels/LinearAlgebra/L01_Module.lean | 6 +-- .../LinearAlgebra/L02_VectorNotation.lean | 4 +- .../LinearAlgebra/L03_VectorNotation.lean | 4 +- .../Levels/LinearAlgebra/L04_Submodule.lean | 4 +- .../Levels/LinearAlgebra/L05_Submodule.lean | 4 +- .../Adam/Levels/LinearAlgebra/L06_Span.lean | 4 +- .../Adam/Levels/LinearAlgebra/L07_Span.lean | 4 +- .../LinearAlgebra/L08_GeneratingSet.lean | 4 +- .../Levels/LinearAlgebra/M01_LinearMap.lean | 4 +- .../Levels/LinearAlgebra/M02_LinearIndep.lean | 4 +- .../Adam/Levels/LinearAlgebra/M04_Basis.lean | 4 +- .../Adam/Levels/LinearAlgebra/N01_Span.lean | 4 +- .../Adam/Levels/LinearAlgebra/N02_Span.lean | 4 +- .../Levels/LinearAlgebra/N03_Idempotent.lean | 4 +- .../Levels/LinearAlgebra/N04_Idempotent.lean | 4 +- .../Adam/Levels/LinearAlgebra/N05_Sum.lean | 4 +- .../Adam/Levels/LinearAlgebra/N06_Sum.lean | 4 +- .../Adam/Levels/LinearAlgebra/N07_Prod.lean | 4 +- .../Adam/Levels/LinearAlgebra/N08_Prod.lean | 4 +- .../Adam/Levels/LinearAlgebra/N09_Prod.lean | 4 +- server/adam/Adam/Levels/Numbers.lean | 4 +- server/adam/Adam/Levels/Numbers/L01_PNat.lean | 4 +- server/adam/Adam/Levels/Numbers/L02_PNat.lean | 4 +- server/adam/Adam/Levels/Predicate.lean | 20 ++++---- .../adam/Adam/Levels/Predicate/L01_Ring.lean | 4 +- .../Adam/Levels/Predicate/L02_Rewrite.lean | 4 +- .../Adam/Levels/Predicate/L03_Rewrite.lean | 4 +- .../adam/Adam/Levels/Predicate/L04_Ring.lean | 4 +- .../adam/Adam/Levels/Predicate/L05_Rfl.lean | 4 +- .../Adam/Levels/Predicate/L06_Exists.lean | 4 +- .../Adam/Levels/Predicate/L07_Exists.lean | 4 +- .../Adam/Levels/Predicate/L08_Forall.lean | 4 +- .../Adam/Levels/Predicate/L09_PushNeg.lean | 6 +-- server/adam/Adam/Levels/Prime.lean | 10 ++-- server/adam/Adam/Levels/Prime/L01_Dvd.lean | 4 +- server/adam/Adam/Levels/Prime/L02_Prime.lean | 6 +-- server/adam/Adam/Levels/Prime/L03_Prime.lean | 6 +-- .../Adam/Levels/Prime/L06_ExistsUnique.lean | 6 +-- server/adam/Adam/Levels/Proposition.lean | 30 ++++++------ .../Adam/Levels/Proposition/L00_Tauto.lean | 4 +- .../adam/Adam/Levels/Proposition/L01_Rfl.lean | 4 +- .../Levels/Proposition/L02_Assumption.lean | 4 +- .../Levels/Proposition/L03_Assumption.lean | 4 +- .../Adam/Levels/Proposition/L04_True.lean | 4 +- .../adam/Adam/Levels/Proposition/L05_Not.lean | 4 +- .../Adam/Levels/Proposition/L06_False.lean | 4 +- .../Levels/Proposition/L07_ContraNotEq.lean | 6 +-- .../Adam/Levels/Proposition/L08_Contra.lean | 6 +-- .../adam/Adam/Levels/Proposition/L09_And.lean | 4 +- .../adam/Adam/Levels/Proposition/L10_And.lean | 4 +- .../adam/Adam/Levels/Proposition/L11_Or.lean | 4 +- .../adam/Adam/Levels/Proposition/L12_Or.lean | 4 +- .../Adam/Levels/Proposition/L13_Summary.lean | 4 +- server/adam/Adam/Levels/SetFunction.lean | 10 ++-- .../Adam/Levels/SetFunction/L01_Image.lean | 4 +- .../Adam/Levels/SetFunction/L02_Preimage.lean | 4 +- .../Adam/Levels/SetFunction/L03_Range.lean | 4 +- .../Levels/SetFunction/L04_ImageUnion.lean | 4 +- server/adam/Adam/Levels/SetTheory.lean | 46 +++++++++---------- .../adam/Adam/Levels/SetTheory/L01_Univ.lean | 4 +- .../adam/Adam/Levels/SetTheory/L02_Empty.lean | 4 +- .../Adam/Levels/SetTheory/L03_Subset.lean | 4 +- .../Levels/SetTheory/L04_SubsetEmpty.lean | 6 +-- .../adam/Adam/Levels/SetTheory/L05_Empty.lean | 6 +-- .../Adam/Levels/SetTheory/L06_Nonempty.lean | 6 +-- .../Adam/Levels/SetTheory/L07_UnionInter.lean | 4 +- .../Adam/Levels/SetTheory/L08_UnionInter.lean | 4 +- .../Adam/Levels/SetTheory/L09_Complement.lean | 4 +- .../Adam/Levels/SetTheory/L10_Morgan.lean | 4 +- .../Adam/Levels/SetTheory/L11_SSubset.lean | 4 +- .../Adam/Levels/SetTheory/L12_Insert.lean | 4 +- .../Adam/Levels/SetTheory/L13_Insert.lean | 4 +- .../adam/Adam/Levels/SetTheory/L14_SetOf.lean | 4 +- .../Adam/Levels/SetTheory/L15_Powerset.lean | 6 +-- .../Adam/Levels/SetTheory/L16_Disjoint.lean | 4 +- .../adam/Adam/Levels/SetTheory/L17_SetOf.lean | 4 +- .../adam/Adam/Levels/SetTheory/L18_SetOf.lean | 4 +- .../Adam/Levels/SetTheory/L19_Subtype.lean | 4 +- .../Adam/Levels/SetTheory/L20_UnionInter.lean | 4 +- .../Adam/Levels/SetTheory/L21_Summary.lean | 4 +- .../adam/Adam/Levels/SetTheory/T01_Set.lean | 4 +- server/adam/Adam/Levels/SetTheory/T04_xx.lean | 4 +- server/adam/Adam/Levels/StatementTest.lean | 4 +- server/adam/Adam/Levels/Sum.lean | 14 +++--- server/adam/Adam/Levels/Sum/L01_Simp.lean | 6 +-- server/adam/Adam/Levels/Sum/L02_Sum.lean | 6 +-- server/adam/Adam/Levels/Sum/L03_ArithSum.lean | 6 +-- server/adam/Adam/Levels/Sum/L04_SumOdd.lean | 6 +-- server/adam/Adam/Levels/Sum/L05_SumComm.lean | 8 ++-- server/adam/Adam/Levels/Sum/L06_Summary.lean | 10 ++-- .../adam/Adam/Levels/Sum/T01_Induction.lean | 6 +-- .../adam/Adam/Levels/Sum/T02_Induction.lean | 6 +-- .../adam/Adam/Levels/Sum/T03__Bernoulli.lean | 8 ++-- server/adam/Adam/Metadata.lean | 4 +- server/adam/Adam/StructInstWithHolesTest.lean | 2 +- server/adam/Adam/TacticDocs.lean | 2 +- server/adam/Adam/Tactics.lean | 2 +- server/adam/lakefile.lean | 4 +- server/build.sh | 10 ++-- server/index.mjs | 6 +-- server/server.Dockerfile | 2 +- 157 files changed, 462 insertions(+), 462 deletions(-) diff --git a/UPDATE_LEAN.sh b/UPDATE_LEAN.sh index 899dbbc..34f979f 100755 --- a/UPDATE_LEAN.sh +++ b/UPDATE_LEAN.sh @@ -5,7 +5,7 @@ cd $(dirname $0) cd server -cd testgame +cd adam lake update cp lake-packages/mathlib/lean-toolchain lean-toolchain diff --git a/client/src/index.tsx b/client/src/index.tsx index eedeb12..20f2ac0 100644 --- a/client/src/index.tsx +++ b/client/src/index.tsx @@ -20,7 +20,7 @@ monacoSetup() const router = createHashRouter([ { path: "/", - loader: () => redirect("/game/testgame") + loader: () => redirect("/game/adam") }, { path: "/game/:gameId", diff --git a/package.json b/package.json index ebe5cdc..fc3bf0a 100644 --- a/package.json +++ b/package.json @@ -56,7 +56,7 @@ }, "scripts": { "start": "concurrently -n server,client -c blue,green \"npm run start_server\" \"npm run start_client\"", - "start_server": "cd server && (cd leanserver && lake build) && (cd testgame && lake exe cache get && lake build) && (cd nng && lake build) && NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\"", + "start_server": "cd server && (cd leanserver && lake build) && (cd adam && lake exe cache get && lake build) && (cd nng && lake build) && NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\"", "start_client": "NODE_ENV=development webpack-dev-server --hot", "build": "npm run build_server && npm run build_client", "build_server": "server/build.sh", diff --git a/server/adam/Adam.lean b/server/adam/Adam.lean index ea0d890..2f5351d 100644 --- a/server/adam/Adam.lean +++ b/server/adam/Adam.lean @@ -1,25 +1,25 @@ -import TestGame.Metadata +import Adam.Metadata -import TestGame.Levels.Proposition -import TestGame.Levels.Implication -import TestGame.Levels.Predicate -import TestGame.Levels.Contradiction --- import TestGame.Levels.Prime -import TestGame.Levels.Sum --- import TestGame.Levels.Induction +import Adam.Levels.Proposition +import Adam.Levels.Implication +import Adam.Levels.Predicate +import Adam.Levels.Contradiction +-- import Adam.Levels.Prime +import Adam.Levels.Sum +-- import Adam.Levels.Induction -import TestGame.Levels.Numbers -import TestGame.Levels.Inequality +import Adam.Levels.Numbers +import Adam.Levels.Inequality -import TestGame.Levels.Lean -import TestGame.Levels.SetTheory -import TestGame.Levels.Function -import TestGame.Levels.SetFunction -import TestGame.Levels.LinearAlgebra +import Adam.Levels.Lean +import Adam.Levels.SetTheory +import Adam.Levels.Function +import Adam.Levels.SetFunction +import Adam.Levels.LinearAlgebra -Game "TestGame" +Game "Adam" Title "Lean 4 game" Introduction " diff --git a/server/adam/Adam/Levels/Contradiction.lean b/server/adam/Adam/Levels/Contradiction.lean index 5805bb1..a7cdde7 100644 --- a/server/adam/Adam/Levels/Contradiction.lean +++ b/server/adam/Adam/Levels/Contradiction.lean @@ -1,11 +1,11 @@ -import TestGame.Levels.Contradiction.L01_Have -import TestGame.Levels.Contradiction.L02_Suffices -import TestGame.Levels.Contradiction.L03_ByContra -import TestGame.Levels.Contradiction.L04_ByContra -import TestGame.Levels.Contradiction.L05_Contrapose -import TestGame.Levels.Contradiction.L06_Summary +import Adam.Levels.Contradiction.L01_Have +import Adam.Levels.Contradiction.L02_Suffices +import Adam.Levels.Contradiction.L03_ByContra +import Adam.Levels.Contradiction.L04_ByContra +import Adam.Levels.Contradiction.L05_Contrapose +import Adam.Levels.Contradiction.L06_Summary -Game "TestGame" +Game "Adam" World "Contradiction" Title "Widerspruch" diff --git a/server/adam/Adam/Levels/Contradiction/L01_Have.lean b/server/adam/Adam/Levels/Contradiction/L01_Have.lean index e80a472..01d4aa3 100644 --- a/server/adam/Adam/Levels/Contradiction/L01_Have.lean +++ b/server/adam/Adam/Levels/Contradiction/L01_Have.lean @@ -1,13 +1,13 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.LeftRight import Mathlib.Tactic.Contrapose import Mathlib.Tactic.Use import Mathlib.Tactic.Ring -import TestGame.ToBePorted +import Adam.ToBePorted -Game "TestGame" +Game "Adam" World "Contradiction" Level 1 diff --git a/server/adam/Adam/Levels/Contradiction/L02_Suffices.lean b/server/adam/Adam/Levels/Contradiction/L02_Suffices.lean index 5480fe4..ac8f762 100644 --- a/server/adam/Adam/Levels/Contradiction/L02_Suffices.lean +++ b/server/adam/Adam/Levels/Contradiction/L02_Suffices.lean @@ -1,13 +1,13 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.LeftRight import Mathlib.Tactic.Contrapose import Mathlib.Tactic.Use import Mathlib.Tactic.Ring -import TestGame.ToBePorted +import Adam.ToBePorted -Game "TestGame" +Game "Adam" World "Contradiction" Level 2 diff --git a/server/adam/Adam/Levels/Contradiction/L03_ByContra.lean b/server/adam/Adam/Levels/Contradiction/L03_ByContra.lean index c9e4013..4a178bf 100644 --- a/server/adam/Adam/Levels/Contradiction/L03_ByContra.lean +++ b/server/adam/Adam/Levels/Contradiction/L03_ByContra.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.LeftRight import Mathlib.Tactic.Contrapose @@ -6,9 +6,9 @@ import Mathlib.Tactic.Use import Mathlib.Tactic.Ring import Mathlib -import TestGame.ToBePorted +import Adam.ToBePorted -Game "TestGame" +Game "Adam" World "Contradiction" Level 3 diff --git a/server/adam/Adam/Levels/Contradiction/L04_ByContra.lean b/server/adam/Adam/Levels/Contradiction/L04_ByContra.lean index 769a4cc..f9530cc 100644 --- a/server/adam/Adam/Levels/Contradiction/L04_ByContra.lean +++ b/server/adam/Adam/Levels/Contradiction/L04_ByContra.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.LeftRight import Mathlib.Tactic.Contrapose @@ -6,9 +6,9 @@ import Mathlib.Tactic.Use import Mathlib.Tactic.Ring import Mathlib -import TestGame.ToBePorted +import Adam.ToBePorted -Game "TestGame" +Game "Adam" World "Contradiction" Level 4 diff --git a/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean b/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean index 6377dec..e2df673 100644 --- a/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean +++ b/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean @@ -1,12 +1,12 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.Contrapose import Mathlib.Tactic.Use import Mathlib.Tactic.Ring -import TestGame.ToBePorted +import Adam.ToBePorted -Game "TestGame" +Game "Adam" World "Contradiction" Level 5 diff --git a/server/adam/Adam/Levels/Contradiction/L06_Summary.lean b/server/adam/Adam/Levels/Contradiction/L06_Summary.lean index 64693b0..1e32524 100644 --- a/server/adam/Adam/Levels/Contradiction/L06_Summary.lean +++ b/server/adam/Adam/Levels/Contradiction/L06_Summary.lean @@ -1,12 +1,12 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.Contrapose import Mathlib.Tactic.Use import Mathlib.Tactic.Ring -import TestGame.ToBePorted +import Adam.ToBePorted -Game "TestGame" +Game "Adam" World "Contradiction" Level 6 diff --git a/server/adam/Adam/Levels/Function.lean b/server/adam/Adam/Levels/Function.lean index 0d2770d..91a8bbe 100644 --- a/server/adam/Adam/Levels/Function.lean +++ b/server/adam/Adam/Levels/Function.lean @@ -1,15 +1,15 @@ -import TestGame.Levels.Function.L01_Function -import TestGame.Levels.Function.L02_Let -import TestGame.Levels.Function.L03_Piecewise -import TestGame.Levels.Function.L04_Injective -import TestGame.Levels.Function.L05_Injective -import TestGame.Levels.Function.L06_Injective -import TestGame.Levels.Function.L07_Surjective -import TestGame.Levels.Function.L08_Bijective -import TestGame.Levels.Function.L09_Inverse -import TestGame.Levels.Function.L11_Inverse +import Adam.Levels.Function.L01_Function +import Adam.Levels.Function.L02_Let +import Adam.Levels.Function.L03_Piecewise +import Adam.Levels.Function.L04_Injective +import Adam.Levels.Function.L05_Injective +import Adam.Levels.Function.L06_Injective +import Adam.Levels.Function.L07_Surjective +import Adam.Levels.Function.L08_Bijective +import Adam.Levels.Function.L09_Inverse +import Adam.Levels.Function.L11_Inverse -Game "TestGame" +Game "Adam" World "Function" Title "Abbildungen" diff --git a/server/adam/Adam/Levels/Function/L01_Function.lean b/server/adam/Adam/Levels/Function/L01_Function.lean index 1bce9e1..52607f9 100644 --- a/server/adam/Adam/Levels/Function/L01_Function.lean +++ b/server/adam/Adam/Levels/Function/L01_Function.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -Game "TestGame" +Game "Adam" World "Function" Level 1 diff --git a/server/adam/Adam/Levels/Function/L02_Let.lean b/server/adam/Adam/Levels/Function/L02_Let.lean index b996425..80c95c6 100644 --- a/server/adam/Adam/Levels/Function/L02_Let.lean +++ b/server/adam/Adam/Levels/Function/L02_Let.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -Game "TestGame" +Game "Adam" World "Function" Level 2 diff --git a/server/adam/Adam/Levels/Function/L03_Piecewise.lean b/server/adam/Adam/Levels/Function/L03_Piecewise.lean index 8c1615b..591a081 100644 --- a/server/adam/Adam/Levels/Function/L03_Piecewise.lean +++ b/server/adam/Adam/Levels/Function/L03_Piecewise.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -Game "TestGame" +Game "Adam" World "Function" Level 3 diff --git a/server/adam/Adam/Levels/Function/L04_Injective.lean b/server/adam/Adam/Levels/Function/L04_Injective.lean index 0946ab4..b21a7fc 100644 --- a/server/adam/Adam/Levels/Function/L04_Injective.lean +++ b/server/adam/Adam/Levels/Function/L04_Injective.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -Game "TestGame" +Game "Adam" World "Function" Level 4 diff --git a/server/adam/Adam/Levels/Function/L05_Injective.lean b/server/adam/Adam/Levels/Function/L05_Injective.lean index 48f0172..17bf39f 100644 --- a/server/adam/Adam/Levels/Function/L05_Injective.lean +++ b/server/adam/Adam/Levels/Function/L05_Injective.lean @@ -1,9 +1,9 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Function" Level 5 diff --git a/server/adam/Adam/Levels/Function/L06_Injective.lean b/server/adam/Adam/Levels/Function/L06_Injective.lean index 4e61007..2335749 100644 --- a/server/adam/Adam/Levels/Function/L06_Injective.lean +++ b/server/adam/Adam/Levels/Function/L06_Injective.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -Game "TestGame" +Game "Adam" World "Function" Level 6 diff --git a/server/adam/Adam/Levels/Function/L07_Surjective.lean b/server/adam/Adam/Levels/Function/L07_Surjective.lean index 27906d8..7f493b3 100644 --- a/server/adam/Adam/Levels/Function/L07_Surjective.lean +++ b/server/adam/Adam/Levels/Function/L07_Surjective.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -Game "TestGame" +Game "Adam" World "Function" Level 7 diff --git a/server/adam/Adam/Levels/Function/L08_Bijective.lean b/server/adam/Adam/Levels/Function/L08_Bijective.lean index c7a2889..98aec98 100644 --- a/server/adam/Adam/Levels/Function/L08_Bijective.lean +++ b/server/adam/Adam/Levels/Function/L08_Bijective.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -Game "TestGame" +Game "Adam" World "Function" Level 8 diff --git a/server/adam/Adam/Levels/Function/L09_Inverse.lean b/server/adam/Adam/Levels/Function/L09_Inverse.lean index 548d01e..120ccbd 100644 --- a/server/adam/Adam/Levels/Function/L09_Inverse.lean +++ b/server/adam/Adam/Levels/Function/L09_Inverse.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -Game "TestGame" +Game "Adam" World "Function" Level 9 diff --git a/server/adam/Adam/Levels/Function/L11_Inverse.lean b/server/adam/Adam/Levels/Function/L11_Inverse.lean index 14ac036..f6b0c68 100644 --- a/server/adam/Adam/Levels/Function/L11_Inverse.lean +++ b/server/adam/Adam/Levels/Function/L11_Inverse.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -Game "TestGame" +Game "Adam" World "Function" Level 10 diff --git a/server/adam/Adam/Levels/Implication.lean b/server/adam/Adam/Levels/Implication.lean index 23e5361..6b77705 100644 --- a/server/adam/Adam/Levels/Implication.lean +++ b/server/adam/Adam/Levels/Implication.lean @@ -1,18 +1,18 @@ -import TestGame.Levels.Implication.L01_Intro -import TestGame.Levels.Implication.L02_Revert -import TestGame.Levels.Implication.L03_Apply -import TestGame.Levels.Implication.L04_Apply -import TestGame.Levels.Implication.L05_Apply -import TestGame.Levels.Implication.L06_Iff -import TestGame.Levels.Implication.L07_Rw -import TestGame.Levels.Implication.L08_Iff -import TestGame.Levels.Implication.L09_Iff -import TestGame.Levels.Implication.L10_Apply -import TestGame.Levels.Implication.L11_ByCases -import TestGame.Levels.Implication.L12_Rw -import TestGame.Levels.Implication.L13_Summary +import Adam.Levels.Implication.L01_Intro +import Adam.Levels.Implication.L02_Revert +import Adam.Levels.Implication.L03_Apply +import Adam.Levels.Implication.L04_Apply +import Adam.Levels.Implication.L05_Apply +import Adam.Levels.Implication.L06_Iff +import Adam.Levels.Implication.L07_Rw +import Adam.Levels.Implication.L08_Iff +import Adam.Levels.Implication.L09_Iff +import Adam.Levels.Implication.L10_Apply +import Adam.Levels.Implication.L11_ByCases +import Adam.Levels.Implication.L12_Rw +import Adam.Levels.Implication.L13_Summary -Game "TestGame" +Game "Adam" World "Implication" Title "Aussagenlogik 2" diff --git a/server/adam/Adam/Levels/Implication/L01_Intro.lean b/server/adam/Adam/Levels/Implication/L01_Intro.lean index 36b9d6d..97fef55 100644 --- a/server/adam/Adam/Levels/Implication/L01_Intro.lean +++ b/server/adam/Adam/Levels/Implication/L01_Intro.lean @@ -1,9 +1,9 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Tactic.Tauto set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Implication" Level 1 diff --git a/server/adam/Adam/Levels/Implication/L02_Revert.lean b/server/adam/Adam/Levels/Implication/L02_Revert.lean index f05a5c9..5345c60 100644 --- a/server/adam/Adam/Levels/Implication/L02_Revert.lean +++ b/server/adam/Adam/Levels/Implication/L02_Revert.lean @@ -1,8 +1,8 @@ -import TestGame.Metadata +import Adam.Metadata set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Implication" Level 2 diff --git a/server/adam/Adam/Levels/Implication/L03_Apply.lean b/server/adam/Adam/Levels/Implication/L03_Apply.lean index 6fa2b33..30eb21f 100644 --- a/server/adam/Adam/Levels/Implication/L03_Apply.lean +++ b/server/adam/Adam/Levels/Implication/L03_Apply.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -Game "TestGame" +Game "Adam" World "Implication" Level 3 diff --git a/server/adam/Adam/Levels/Implication/L04_Apply.lean b/server/adam/Adam/Levels/Implication/L04_Apply.lean index 1d4a7a9..bef022c 100644 --- a/server/adam/Adam/Levels/Implication/L04_Apply.lean +++ b/server/adam/Adam/Levels/Implication/L04_Apply.lean @@ -1,8 +1,8 @@ -import TestGame.Metadata +import Adam.Metadata set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Implication" Level 4 diff --git a/server/adam/Adam/Levels/Implication/L05_Apply.lean b/server/adam/Adam/Levels/Implication/L05_Apply.lean index 90fa447..ef92b93 100644 --- a/server/adam/Adam/Levels/Implication/L05_Apply.lean +++ b/server/adam/Adam/Levels/Implication/L05_Apply.lean @@ -1,6 +1,6 @@ -import TestGame.Metadata +import Adam.Metadata -Game "TestGame" +Game "Adam" World "Implication" Level 5 diff --git a/server/adam/Adam/Levels/Implication/L06_Iff.lean b/server/adam/Adam/Levels/Implication/L06_Iff.lean index 84a4130..3941d32 100644 --- a/server/adam/Adam/Levels/Implication/L06_Iff.lean +++ b/server/adam/Adam/Levels/Implication/L06_Iff.lean @@ -1,6 +1,6 @@ -import TestGame.Metadata +import Adam.Metadata -Game "TestGame" +Game "Adam" World "Implication" Level 6 diff --git a/server/adam/Adam/Levels/Implication/L07_Rw.lean b/server/adam/Adam/Levels/Implication/L07_Rw.lean index d984d80..dc1fa5d 100644 --- a/server/adam/Adam/Levels/Implication/L07_Rw.lean +++ b/server/adam/Adam/Levels/Implication/L07_Rw.lean @@ -1,11 +1,11 @@ -import TestGame.Metadata +import Adam.Metadata import Init.Data.ToString -- #check List UInt8 set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Implication" Level 7 diff --git a/server/adam/Adam/Levels/Implication/L08_Iff.lean b/server/adam/Adam/Levels/Implication/L08_Iff.lean index 8801210..0cd443d 100644 --- a/server/adam/Adam/Levels/Implication/L08_Iff.lean +++ b/server/adam/Adam/Levels/Implication/L08_Iff.lean @@ -1,8 +1,8 @@ -import TestGame.Metadata +import Adam.Metadata set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Implication" Level 8 diff --git a/server/adam/Adam/Levels/Implication/L09_Iff.lean b/server/adam/Adam/Levels/Implication/L09_Iff.lean index daede52..60835df 100644 --- a/server/adam/Adam/Levels/Implication/L09_Iff.lean +++ b/server/adam/Adam/Levels/Implication/L09_Iff.lean @@ -1,8 +1,8 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.Cases -Game "TestGame" +Game "Adam" World "Implication" Level 9 diff --git a/server/adam/Adam/Levels/Implication/L10_Apply.lean b/server/adam/Adam/Levels/Implication/L10_Apply.lean index 8905f6f..5e47099 100644 --- a/server/adam/Adam/Levels/Implication/L10_Apply.lean +++ b/server/adam/Adam/Levels/Implication/L10_Apply.lean @@ -1,9 +1,9 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.Cases import Mathlib -Game "TestGame" +Game "Adam" World "Implication" Level 10 diff --git a/server/adam/Adam/Levels/Implication/L11_ByCases.lean b/server/adam/Adam/Levels/Implication/L11_ByCases.lean index 7493335..d5048b4 100644 --- a/server/adam/Adam/Levels/Implication/L11_ByCases.lean +++ b/server/adam/Adam/Levels/Implication/L11_ByCases.lean @@ -1,9 +1,9 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.Cases import Mathlib -Game "TestGame" +Game "Adam" World "Implication" Level 11 diff --git a/server/adam/Adam/Levels/Implication/L12_Rw.lean b/server/adam/Adam/Levels/Implication/L12_Rw.lean index ed9683a..5685c3a 100644 --- a/server/adam/Adam/Levels/Implication/L12_Rw.lean +++ b/server/adam/Adam/Levels/Implication/L12_Rw.lean @@ -1,9 +1,9 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.Cases import Mathlib.Logic.Basic -Game "TestGame" +Game "Adam" World "Implication" Level 12 diff --git a/server/adam/Adam/Levels/Implication/L13_Summary.lean b/server/adam/Adam/Levels/Implication/L13_Summary.lean index 6de3e35..0e86aad 100644 --- a/server/adam/Adam/Levels/Implication/L13_Summary.lean +++ b/server/adam/Adam/Levels/Implication/L13_Summary.lean @@ -1,11 +1,11 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.LeftRight import Mathlib set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Implication" Level 13 diff --git a/server/adam/Adam/Levels/Induction.lean b/server/adam/Adam/Levels/Induction.lean index c79daa1..5e77bb6 100644 --- a/server/adam/Adam/Levels/Induction.lean +++ b/server/adam/Adam/Levels/Induction.lean @@ -1,5 +1,5 @@ -import TestGame.Levels.Induction.L01_Induction +import Adam.Levels.Induction.L01_Induction -Game "TestGame" +Game "Adam" World "Induction" Title "Übungen Induktions" diff --git a/server/adam/Adam/Levels/Induction/L01_Induction.lean b/server/adam/Adam/Levels/Induction/L01_Induction.lean index f2804b9..66a8473 100644 --- a/server/adam/Adam/Levels/Induction/L01_Induction.lean +++ b/server/adam/Adam/Levels/Induction/L01_Induction.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Induction" Level 1 diff --git a/server/adam/Adam/Levels/Inequality.lean b/server/adam/Adam/Levels/Inequality.lean index b1684b6..d136814 100644 --- a/server/adam/Adam/Levels/Inequality.lean +++ b/server/adam/Adam/Levels/Inequality.lean @@ -1,9 +1,9 @@ -import TestGame.Levels.Inequality.L01_LE -import TestGame.Levels.Inequality.L02_Pos -import TestGame.Levels.Inequality.L03_Linarith -import TestGame.Levels.Inequality.L04_Linarith +import Adam.Levels.Inequality.L01_LE +import Adam.Levels.Inequality.L02_Pos +import Adam.Levels.Inequality.L03_Linarith +import Adam.Levels.Inequality.L04_Linarith -Game "TestGame" +Game "Adam" World "Inequality" Title "Ungleichung" diff --git a/server/adam/Adam/Levels/Inequality/L01_LE.lean b/server/adam/Adam/Levels/Inequality/L01_LE.lean index d03dcce..eaebe8b 100644 --- a/server/adam/Adam/Levels/Inequality/L01_LE.lean +++ b/server/adam/Adam/Levels/Inequality/L01_LE.lean @@ -1,6 +1,6 @@ -import TestGame.Metadata +import Adam.Metadata -Game "TestGame" +Game "Adam" World "Inequality" Level 1 diff --git a/server/adam/Adam/Levels/Inequality/L02_Pos.lean b/server/adam/Adam/Levels/Inequality/L02_Pos.lean index 8dbb898..e328984 100644 --- a/server/adam/Adam/Levels/Inequality/L02_Pos.lean +++ b/server/adam/Adam/Levels/Inequality/L02_Pos.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Tactic.LibrarySearch set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Inequality" Level 2 diff --git a/server/adam/Adam/Levels/Inequality/L03_Linarith.lean b/server/adam/Adam/Levels/Inequality/L03_Linarith.lean index 83c551c..bec5fdb 100644 --- a/server/adam/Adam/Levels/Inequality/L03_Linarith.lean +++ b/server/adam/Adam/Levels/Inequality/L03_Linarith.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Tactic.Linarith -Game "TestGame" +Game "Adam" World "Inequality" Level 3 diff --git a/server/adam/Adam/Levels/Inequality/L04_Linarith.lean b/server/adam/Adam/Levels/Inequality/L04_Linarith.lean index b688b02..0cb1618 100644 --- a/server/adam/Adam/Levels/Inequality/L04_Linarith.lean +++ b/server/adam/Adam/Levels/Inequality/L04_Linarith.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Tactic.Linarith -Game "TestGame" +Game "Adam" World "Inequality" Level 4 diff --git a/server/adam/Adam/Levels/Inequality/T_Induction.lean b/server/adam/Adam/Levels/Inequality/T_Induction.lean index a393275..0d0830b 100644 --- a/server/adam/Adam/Levels/Inequality/T_Induction.lean +++ b/server/adam/Adam/Levels/Inequality/T_Induction.lean @@ -1,8 +1,8 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -Game "TestGame" +Game "Adam" World "Inequality" Level 1 diff --git a/server/adam/Adam/Levels/Lean.lean b/server/adam/Adam/Levels/Lean.lean index 849ce7c..ff5f672 100644 --- a/server/adam/Adam/Levels/Lean.lean +++ b/server/adam/Adam/Levels/Lean.lean @@ -1,9 +1,9 @@ -import TestGame.Levels.Lean.L01_Type -import TestGame.Levels.Lean.L02_Universe -import TestGame.Levels.Lean.L03_ImplicitArguments -import TestGame.Levels.Lean.L04_InstanceArguments +import Adam.Levels.Lean.L01_Type +import Adam.Levels.Lean.L02_Universe +import Adam.Levels.Lean.L03_ImplicitArguments +import Adam.Levels.Lean.L04_InstanceArguments -Game "TestGame" +Game "Adam" World "Lean" Title "Lean" diff --git a/server/adam/Adam/Levels/Lean/L01_Type.lean b/server/adam/Adam/Levels/Lean/L01_Type.lean index 079051d..eb4a62d 100644 --- a/server/adam/Adam/Levels/Lean/L01_Type.lean +++ b/server/adam/Adam/Levels/Lean/L01_Type.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Lean" Level 1 diff --git a/server/adam/Adam/Levels/Lean/L02_Universe.lean b/server/adam/Adam/Levels/Lean/L02_Universe.lean index 9566a99..c20c171 100644 --- a/server/adam/Adam/Levels/Lean/L02_Universe.lean +++ b/server/adam/Adam/Levels/Lean/L02_Universe.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Lean" Level 2 diff --git a/server/adam/Adam/Levels/Lean/L03_ImplicitArguments.lean b/server/adam/Adam/Levels/Lean/L03_ImplicitArguments.lean index 3b1c398..19a8411 100644 --- a/server/adam/Adam/Levels/Lean/L03_ImplicitArguments.lean +++ b/server/adam/Adam/Levels/Lean/L03_ImplicitArguments.lean @@ -1,11 +1,11 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -import TestGame.ToBePorted +import Adam.ToBePorted set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Lean" Level 3 diff --git a/server/adam/Adam/Levels/Lean/L04_InstanceArguments.lean b/server/adam/Adam/Levels/Lean/L04_InstanceArguments.lean index 10da5bc..dbb5425 100644 --- a/server/adam/Adam/Levels/Lean/L04_InstanceArguments.lean +++ b/server/adam/Adam/Levels/Lean/L04_InstanceArguments.lean @@ -1,11 +1,11 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -import TestGame.ToBePorted +import Adam.ToBePorted set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Lean" Level 4 diff --git a/server/adam/Adam/Levels/LeftOvers/L09_Or.lean b/server/adam/Adam/Levels/LeftOvers/L09_Or.lean index 24297d5..b572c8a 100644 --- a/server/adam/Adam/Levels/LeftOvers/L09_Or.lean +++ b/server/adam/Adam/Levels/LeftOvers/L09_Or.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.LeftRight set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Implication" Level 9 diff --git a/server/adam/Adam/Levels/LeftOvers/L33_Prime.lean b/server/adam/Adam/Levels/LeftOvers/L33_Prime.lean index 1b8393f..419f94a 100644 --- a/server/adam/Adam/Levels/LeftOvers/L33_Prime.lean +++ b/server/adam/Adam/Levels/LeftOvers/L33_Prime.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Tactic.Ring -Game "TestGame" +Game "Adam" World "Nat2" Level 3 diff --git a/server/adam/Adam/Levels/LeftOvers/L34_ExistsUnique.lean b/server/adam/Adam/Levels/LeftOvers/L34_ExistsUnique.lean index 9abc351..49188d0 100644 --- a/server/adam/Adam/Levels/LeftOvers/L34_ExistsUnique.lean +++ b/server/adam/Adam/Levels/LeftOvers/L34_ExistsUnique.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Tactic.Ring -Game "TestGame" +Game "Adam" World "Nat2" Level 5 diff --git a/server/adam/Adam/Levels/LeftOvers/Lxx_Prime.lean b/server/adam/Adam/Levels/LeftOvers/Lxx_Prime.lean index be43277..f1847f8 100644 --- a/server/adam/Adam/Levels/LeftOvers/Lxx_Prime.lean +++ b/server/adam/Adam/Levels/LeftOvers/Lxx_Prime.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.Contrapose import Mathlib.Tactic.Use @@ -21,7 +21,7 @@ lemma even_square (n : ℕ) : even n → even (n ^ 2) := by def prime (n : ℕ) : Prop := (2 ≤ n) ∧ ∀ a b, n = a * b → a = 1 ∨ b = 1 -Game "TestGame" +Game "Adam" World "Nat" Level 4 diff --git a/server/adam/Adam/Levels/LeftOvers/Playground.lean b/server/adam/Adam/Levels/LeftOvers/Playground.lean index 7622e0b..b1f5e6a 100644 --- a/server/adam/Adam/Levels/LeftOvers/Playground.lean +++ b/server/adam/Adam/Levels/LeftOvers/Playground.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -- -- INCORPORATED diff --git a/server/adam/Adam/Levels/LeftOvers/xx_Functions.lean b/server/adam/Adam/Levels/LeftOvers/xx_Functions.lean index 061d9a7..87d457f 100644 --- a/server/adam/Adam/Levels/LeftOvers/xx_Functions.lean +++ b/server/adam/Adam/Levels/LeftOvers/xx_Functions.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Tactic.Ring -Game "TestGame" +Game "Adam" World "Function" Level 1 diff --git a/server/adam/Adam/Levels/LinearAlgebra.lean b/server/adam/Adam/Levels/LinearAlgebra.lean index 6054c79..0bb386d 100644 --- a/server/adam/Adam/Levels/LinearAlgebra.lean +++ b/server/adam/Adam/Levels/LinearAlgebra.lean @@ -1,27 +1,27 @@ -import TestGame.Levels.LinearAlgebra.L01_Module -import TestGame.Levels.LinearAlgebra.L02_VectorNotation -import TestGame.Levels.LinearAlgebra.L03_VectorNotation -import TestGame.Levels.LinearAlgebra.L04_Submodule -import TestGame.Levels.LinearAlgebra.L05_Submodule -import TestGame.Levels.LinearAlgebra.L06_Span -import TestGame.Levels.LinearAlgebra.L07_Span -import TestGame.Levels.LinearAlgebra.L08_GeneratingSet +import Adam.Levels.LinearAlgebra.L01_Module +import Adam.Levels.LinearAlgebra.L02_VectorNotation +import Adam.Levels.LinearAlgebra.L03_VectorNotation +import Adam.Levels.LinearAlgebra.L04_Submodule +import Adam.Levels.LinearAlgebra.L05_Submodule +import Adam.Levels.LinearAlgebra.L06_Span +import Adam.Levels.LinearAlgebra.L07_Span +import Adam.Levels.LinearAlgebra.L08_GeneratingSet -import TestGame.Levels.LinearAlgebra.M01_LinearMap -import TestGame.Levels.LinearAlgebra.M02_LinearIndep -import TestGame.Levels.LinearAlgebra.M04_Basis +import Adam.Levels.LinearAlgebra.M01_LinearMap +import Adam.Levels.LinearAlgebra.M02_LinearIndep +import Adam.Levels.LinearAlgebra.M04_Basis -import TestGame.Levels.LinearAlgebra.N01_Span -import TestGame.Levels.LinearAlgebra.N02_Span -import TestGame.Levels.LinearAlgebra.N03_Idempotent -import TestGame.Levels.LinearAlgebra.N04_Idempotent -import TestGame.Levels.LinearAlgebra.N05_Sum -import TestGame.Levels.LinearAlgebra.N06_Sum -import TestGame.Levels.LinearAlgebra.N07_Prod -import TestGame.Levels.LinearAlgebra.N08_Prod -import TestGame.Levels.LinearAlgebra.N09_Prod +import Adam.Levels.LinearAlgebra.N01_Span +import Adam.Levels.LinearAlgebra.N02_Span +import Adam.Levels.LinearAlgebra.N03_Idempotent +import Adam.Levels.LinearAlgebra.N04_Idempotent +import Adam.Levels.LinearAlgebra.N05_Sum +import Adam.Levels.LinearAlgebra.N06_Sum +import Adam.Levels.LinearAlgebra.N07_Prod +import Adam.Levels.LinearAlgebra.N08_Prod +import Adam.Levels.LinearAlgebra.N09_Prod -Game "TestGame" +Game "Adam" World "Module" Title "Vektorraum" @@ -32,10 +32,10 @@ einer Einführungsvorlesung antrifft: Man definiert ein \"Modul\" (Plural: Modul über einem Ring. Ein Modul über einem *Körper* wird dann auch \"Vektorraum\" genannt. " -Game "TestGame" +Game "Adam" World "Basis" Title "Lineare Abbildungen" -Game "TestGame" +Game "Adam" World "Module2" Title "Mehr Vektorräume" diff --git a/server/adam/Adam/Levels/LinearAlgebra/L01_Module.lean b/server/adam/Adam/Levels/LinearAlgebra/L01_Module.lean index e0c0082..d1866ec 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/L01_Module.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/L01_Module.lean @@ -1,13 +1,13 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Real.Basic -- definiert `ℝ` import Mathlib.Algebra.Module.Basic -- definiert `module` import Mathlib.Tactic.LibrarySearch -import TestGame.StructInstWithHoles +import Adam.StructInstWithHoles set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Module" Level 1 diff --git a/server/adam/Adam/Levels/LinearAlgebra/L02_VectorNotation.lean b/server/adam/Adam/Levels/LinearAlgebra/L02_VectorNotation.lean index ad71161..c0b6be3 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/L02_VectorNotation.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/L02_VectorNotation.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Real.Basic -- definiert `ℝ` import Mathlib.Algebra.Module.Pi -- definiert `Module ℚ (fin 2 → ℚ)` @@ -7,7 +7,7 @@ import Mathlib.Tactic.FinCases set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Module" Level 2 diff --git a/server/adam/Adam/Levels/LinearAlgebra/L03_VectorNotation.lean b/server/adam/Adam/Levels/LinearAlgebra/L03_VectorNotation.lean index 839bd94..b49b982 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/L03_VectorNotation.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/L03_VectorNotation.lean @@ -1,11 +1,11 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Real.Basic -- definiert `ℝ` import Mathlib.Algebra.Module.Pi -- definiert `Module ℚ (fin 2 → ℚ)` import Mathlib.Data.Fin.VecNotation import Mathlib.Tactic.FinCases -Game "TestGame" +Game "Adam" World "Module" Level 3 diff --git a/server/adam/Adam/Levels/LinearAlgebra/L04_Submodule.lean b/server/adam/Adam/Levels/LinearAlgebra/L04_Submodule.lean index 42667d3..964e47a 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/L04_Submodule.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/L04_Submodule.lean @@ -1,8 +1,8 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Algebra.Module.Submodule.Lattice -Game "TestGame" +Game "Adam" World "Module" Level 4 diff --git a/server/adam/Adam/Levels/LinearAlgebra/L05_Submodule.lean b/server/adam/Adam/Levels/LinearAlgebra/L05_Submodule.lean index 860a2aa..6709165 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/L05_Submodule.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/L05_Submodule.lean @@ -1,8 +1,8 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Algebra.Module.Submodule.Lattice -Game "TestGame" +Game "Adam" World "Module" Level 5 diff --git a/server/adam/Adam/Levels/LinearAlgebra/L06_Span.lean b/server/adam/Adam/Levels/LinearAlgebra/L06_Span.lean index ae9b8ab..8d309d0 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/L06_Span.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/L06_Span.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Algebra.Module.Submodule.Lattice import Mathlib.Data.Real.Basic -- definiert `ℝ` @@ -8,7 +8,7 @@ import Mathlib.Tactic.FinCases import Mathlib.Algebra.BigOperators.Finsupp -- default? import Mathlib.LinearAlgebra.Span -Game "TestGame" +Game "Adam" World "Module" Level 6 diff --git a/server/adam/Adam/Levels/LinearAlgebra/L07_Span.lean b/server/adam/Adam/Levels/LinearAlgebra/L07_Span.lean index f047823..a50946b 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/L07_Span.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/L07_Span.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Algebra.Module.Submodule.Lattice import Mathlib.Data.Real.Basic -- definiert `ℝ` @@ -10,7 +10,7 @@ import Mathlib.LinearAlgebra.Span import Mathlib.Tactic.LibrarySearch import Mathlib -Game "TestGame" +Game "Adam" World "Module" Level 7 diff --git a/server/adam/Adam/Levels/LinearAlgebra/L08_GeneratingSet.lean b/server/adam/Adam/Levels/LinearAlgebra/L08_GeneratingSet.lean index 32bc7bd..9d20601 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/L08_GeneratingSet.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/L08_GeneratingSet.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Algebra.Module.Submodule.Lattice import Mathlib.Data.Real.Basic -- definiert `ℝ` @@ -8,7 +8,7 @@ import Mathlib.Tactic.FinCases import Mathlib.Algebra.BigOperators.Finsupp -- default? import Mathlib.LinearAlgebra.Span -Game "TestGame" +Game "Adam" World "Module" Level 8 diff --git a/server/adam/Adam/Levels/LinearAlgebra/M01_LinearMap.lean b/server/adam/Adam/Levels/LinearAlgebra/M01_LinearMap.lean index bf6d590..258e0d4 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/M01_LinearMap.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/M01_LinearMap.lean @@ -1,11 +1,11 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Real.Basic -- definiert `ℝ` import Mathlib.Algebra.Module.LinearMap -- definiert `→ₗ` import Mathlib.Tactic.FinCases import Mathlib.Data.Fin.VecNotation -Game "TestGame" +Game "Adam" World "Basis" Level 1 diff --git a/server/adam/Adam/Levels/LinearAlgebra/M02_LinearIndep.lean b/server/adam/Adam/Levels/LinearAlgebra/M02_LinearIndep.lean index a6d0d4e..359fe45 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/M02_LinearIndep.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/M02_LinearIndep.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Algebra.Module.Submodule.Lattice import Mathlib.Data.Real.Basic -- definiert `ℝ` @@ -10,7 +10,7 @@ import Mathlib.Algebra.BigOperators.Basic -- default -- import Mathlib.LinearAlgebra.LinearIndependent import Mathlib -Game "TestGame" +Game "Adam" World "Basis" Level 2 diff --git a/server/adam/Adam/Levels/LinearAlgebra/M04_Basis.lean b/server/adam/Adam/Levels/LinearAlgebra/M04_Basis.lean index 25b5553..c8145e1 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/M04_Basis.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/M04_Basis.lean @@ -1,9 +1,9 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Algebra.Module.Submodule.Lattice import Mathlib -Game "TestGame" +Game "Adam" World "Basis" Level 4 diff --git a/server/adam/Adam/Levels/LinearAlgebra/N01_Span.lean b/server/adam/Adam/Levels/LinearAlgebra/N01_Span.lean index b8d587a..c9d4aaf 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/N01_Span.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/N01_Span.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Algebra.Module.Submodule.Lattice import Mathlib.Data.Real.Basic -- definiert `ℝ` @@ -8,7 +8,7 @@ import Mathlib.Tactic.FinCases import Mathlib.Algebra.BigOperators.Finsupp -- default? import Mathlib.LinearAlgebra.Span -Game "TestGame" +Game "Adam" World "Module2" Level 1 diff --git a/server/adam/Adam/Levels/LinearAlgebra/N02_Span.lean b/server/adam/Adam/Levels/LinearAlgebra/N02_Span.lean index 8d2e82c..decc953 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/N02_Span.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/N02_Span.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Algebra.Module.Submodule.Lattice import Mathlib.Data.Real.Basic -- definiert `ℝ` @@ -11,7 +11,7 @@ import Mathlib open Submodule -Game "TestGame" +Game "Adam" World "Module2" Level 2 diff --git a/server/adam/Adam/Levels/LinearAlgebra/N03_Idempotent.lean b/server/adam/Adam/Levels/LinearAlgebra/N03_Idempotent.lean index 02cf3b4..ceb7558 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/N03_Idempotent.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/N03_Idempotent.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Algebra.Module.Submodule.Lattice import Mathlib.Data.Real.Basic import Mathlib.LinearAlgebra.Basic -Game "TestGame" +Game "Adam" World "Module2" Level 3 diff --git a/server/adam/Adam/Levels/LinearAlgebra/N04_Idempotent.lean b/server/adam/Adam/Levels/LinearAlgebra/N04_Idempotent.lean index 26a956d..fecaebb 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/N04_Idempotent.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/N04_Idempotent.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Algebra.Module.Submodule.Lattice import Mathlib.Data.Real.Basic import Mathlib.LinearAlgebra.Basic -Game "TestGame" +Game "Adam" World "Module2" Level 4 diff --git a/server/adam/Adam/Levels/LinearAlgebra/N05_Sum.lean b/server/adam/Adam/Levels/LinearAlgebra/N05_Sum.lean index 0490708..18ad88c 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/N05_Sum.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/N05_Sum.lean @@ -1,11 +1,11 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Algebra.Module.Submodule.Lattice import Mathlib.LinearAlgebra.Span open Submodule -Game "TestGame" +Game "Adam" World "Module2" Level 5 diff --git a/server/adam/Adam/Levels/LinearAlgebra/N06_Sum.lean b/server/adam/Adam/Levels/LinearAlgebra/N06_Sum.lean index a4655c3..d571449 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/N06_Sum.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/N06_Sum.lean @@ -1,11 +1,11 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Algebra.Module.Submodule.Lattice import Mathlib.LinearAlgebra.Span open Submodule -Game "TestGame" +Game "Adam" World "Module2" Level 6 diff --git a/server/adam/Adam/Levels/LinearAlgebra/N07_Prod.lean b/server/adam/Adam/Levels/LinearAlgebra/N07_Prod.lean index 606d3c5..ff1f973 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/N07_Prod.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/N07_Prod.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Algebra.Module.Submodule.Lattice import Mathlib.Data.Real.Basic import Mathlib.LinearAlgebra.Span -Game "TestGame" +Game "Adam" World "Module2" Level 7 diff --git a/server/adam/Adam/Levels/LinearAlgebra/N08_Prod.lean b/server/adam/Adam/Levels/LinearAlgebra/N08_Prod.lean index 853c9dd..3dcc9a0 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/N08_Prod.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/N08_Prod.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Algebra.Module.Submodule.Lattice import Mathlib.Data.Real.Basic @@ -6,7 +6,7 @@ import Mathlib.LinearAlgebra.Span universe u -Game "TestGame" +Game "Adam" World "Module2" Level 8 diff --git a/server/adam/Adam/Levels/LinearAlgebra/N09_Prod.lean b/server/adam/Adam/Levels/LinearAlgebra/N09_Prod.lean index 0764a87..5b08aa3 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/N09_Prod.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/N09_Prod.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Algebra.Module.Submodule.Lattice import Mathlib.Data.Real.Basic import Mathlib.LinearAlgebra.Span -Game "TestGame" +Game "Adam" World "Module2" Level 9 diff --git a/server/adam/Adam/Levels/Numbers.lean b/server/adam/Adam/Levels/Numbers.lean index 622c5a4..6a6f2fa 100644 --- a/server/adam/Adam/Levels/Numbers.lean +++ b/server/adam/Adam/Levels/Numbers.lean @@ -1,2 +1,2 @@ -import TestGame.Levels.Numbers.L01_PNat -import TestGame.Levels.Numbers.L02_PNat +import Adam.Levels.Numbers.L01_PNat +import Adam.Levels.Numbers.L02_PNat diff --git a/server/adam/Adam/Levels/Numbers/L01_PNat.lean b/server/adam/Adam/Levels/Numbers/L01_PNat.lean index fa1a217..d45f07a 100644 --- a/server/adam/Adam/Levels/Numbers/L01_PNat.lean +++ b/server/adam/Adam/Levels/Numbers/L01_PNat.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -Game "TestGame" +Game "Adam" World "Numbers" Level 1 diff --git a/server/adam/Adam/Levels/Numbers/L02_PNat.lean b/server/adam/Adam/Levels/Numbers/L02_PNat.lean index bca2e8f..b073a3c 100644 --- a/server/adam/Adam/Levels/Numbers/L02_PNat.lean +++ b/server/adam/Adam/Levels/Numbers/L02_PNat.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -Game "TestGame" +Game "Adam" World "Numbers" Level 2 diff --git a/server/adam/Adam/Levels/Predicate.lean b/server/adam/Adam/Levels/Predicate.lean index d5c4135..de8b91a 100644 --- a/server/adam/Adam/Levels/Predicate.lean +++ b/server/adam/Adam/Levels/Predicate.lean @@ -1,14 +1,14 @@ -import TestGame.Levels.Predicate.L01_Ring -import TestGame.Levels.Predicate.L02_Rewrite -import TestGame.Levels.Predicate.L03_Rewrite -import TestGame.Levels.Predicate.L04_Ring -import TestGame.Levels.Predicate.L05_Rfl -import TestGame.Levels.Predicate.L06_Exists -import TestGame.Levels.Predicate.L07_Exists -import TestGame.Levels.Predicate.L08_Forall -import TestGame.Levels.Predicate.L09_PushNeg +import Adam.Levels.Predicate.L01_Ring +import Adam.Levels.Predicate.L02_Rewrite +import Adam.Levels.Predicate.L03_Rewrite +import Adam.Levels.Predicate.L04_Ring +import Adam.Levels.Predicate.L05_Rfl +import Adam.Levels.Predicate.L06_Exists +import Adam.Levels.Predicate.L07_Exists +import Adam.Levels.Predicate.L08_Forall +import Adam.Levels.Predicate.L09_PushNeg -Game "TestGame" +Game "Adam" World "Predicate" Title "Prädikate" diff --git a/server/adam/Adam/Levels/Predicate/L01_Ring.lean b/server/adam/Adam/Levels/Predicate/L01_Ring.lean index ca8b143..fe84bac 100644 --- a/server/adam/Adam/Levels/Predicate/L01_Ring.lean +++ b/server/adam/Adam/Levels/Predicate/L01_Ring.lean @@ -1,9 +1,9 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Tactic.Ring --set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Predicate" Level 1 diff --git a/server/adam/Adam/Levels/Predicate/L02_Rewrite.lean b/server/adam/Adam/Levels/Predicate/L02_Rewrite.lean index a45d6cf..0585180 100644 --- a/server/adam/Adam/Levels/Predicate/L02_Rewrite.lean +++ b/server/adam/Adam/Levels/Predicate/L02_Rewrite.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -Game "TestGame" +Game "Adam" World "Predicate" Level 2 diff --git a/server/adam/Adam/Levels/Predicate/L03_Rewrite.lean b/server/adam/Adam/Levels/Predicate/L03_Rewrite.lean index be4df47..b841059 100644 --- a/server/adam/Adam/Levels/Predicate/L03_Rewrite.lean +++ b/server/adam/Adam/Levels/Predicate/L03_Rewrite.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -Game "TestGame" +Game "Adam" World "Predicate" Level 3 diff --git a/server/adam/Adam/Levels/Predicate/L04_Ring.lean b/server/adam/Adam/Levels/Predicate/L04_Ring.lean index 60291dc..8dd287f 100644 --- a/server/adam/Adam/Levels/Predicate/L04_Ring.lean +++ b/server/adam/Adam/Levels/Predicate/L04_Ring.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Tactic.Ring -Game "TestGame" +Game "Adam" World "Predicate" Level 4 diff --git a/server/adam/Adam/Levels/Predicate/L05_Rfl.lean b/server/adam/Adam/Levels/Predicate/L05_Rfl.lean index e621f96..39b0ee3 100644 --- a/server/adam/Adam/Levels/Predicate/L05_Rfl.lean +++ b/server/adam/Adam/Levels/Predicate/L05_Rfl.lean @@ -1,6 +1,6 @@ -import TestGame.Metadata +import Adam.Metadata -Game "TestGame" +Game "Adam" World "Predicate" Level 5 diff --git a/server/adam/Adam/Levels/Predicate/L06_Exists.lean b/server/adam/Adam/Levels/Predicate/L06_Exists.lean index 79fd82b..f9d91be 100644 --- a/server/adam/Adam/Levels/Predicate/L06_Exists.lean +++ b/server/adam/Adam/Levels/Predicate/L06_Exists.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.Contrapose import Mathlib.Tactic.Use @@ -8,7 +8,7 @@ import Mathlib.Algebra.Parity set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Predicate" Level 6 diff --git a/server/adam/Adam/Levels/Predicate/L07_Exists.lean b/server/adam/Adam/Levels/Predicate/L07_Exists.lean index 26bb955..353b39e 100644 --- a/server/adam/Adam/Levels/Predicate/L07_Exists.lean +++ b/server/adam/Adam/Levels/Predicate/L07_Exists.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.Contrapose import Mathlib.Tactic.Use @@ -8,7 +8,7 @@ import Mathlib.Algebra.Parity set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Predicate" Level 7 diff --git a/server/adam/Adam/Levels/Predicate/L08_Forall.lean b/server/adam/Adam/Levels/Predicate/L08_Forall.lean index ff581b2..0e019e4 100644 --- a/server/adam/Adam/Levels/Predicate/L08_Forall.lean +++ b/server/adam/Adam/Levels/Predicate/L08_Forall.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.Contrapose import Mathlib.Tactic.Use @@ -7,7 +7,7 @@ import Mathlib.Tactic.Ring import Mathlib.Algebra.Parity import Mathlib -Game "TestGame" +Game "Adam" World "Predicate" Level 8 diff --git a/server/adam/Adam/Levels/Predicate/L09_PushNeg.lean b/server/adam/Adam/Levels/Predicate/L09_PushNeg.lean index 7d5bf80..0c5bc91 100644 --- a/server/adam/Adam/Levels/Predicate/L09_PushNeg.lean +++ b/server/adam/Adam/Levels/Predicate/L09_PushNeg.lean @@ -1,12 +1,12 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Tactic.PushNeg import Mathlib import Mathlib.Algebra.Parity -import TestGame.ToBePorted +import Adam.ToBePorted -Game "TestGame" +Game "Adam" World "Predicate" Level 9 diff --git a/server/adam/Adam/Levels/Prime.lean b/server/adam/Adam/Levels/Prime.lean index 51c241c..6f1e466 100644 --- a/server/adam/Adam/Levels/Prime.lean +++ b/server/adam/Adam/Levels/Prime.lean @@ -1,9 +1,9 @@ -import TestGame.Levels.Prime.L01_Dvd --- import TestGame.Levels.Prime.L04_Prime --- import TestGame.Levels.Prime.L05_Prime --- import TestGame.Levels.Prime.L06_ExistsUnique +import Adam.Levels.Prime.L01_Dvd +-- import Adam.Levels.Prime.L04_Prime +-- import Adam.Levels.Prime.L05_Prime +-- import Adam.Levels.Prime.L06_ExistsUnique -Game "TestGame" +Game "Adam" World "Prime" Title "Teilbarkeit" diff --git a/server/adam/Adam/Levels/Prime/L01_Dvd.lean b/server/adam/Adam/Levels/Prime/L01_Dvd.lean index 89f93c8..5e826eb 100644 --- a/server/adam/Adam/Levels/Prime/L01_Dvd.lean +++ b/server/adam/Adam/Levels/Prime/L01_Dvd.lean @@ -1,9 +1,9 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Tactic.Ring import Mathlib -Game "TestGame" +Game "Adam" World "Prime" Level 1 diff --git a/server/adam/Adam/Levels/Prime/L02_Prime.lean b/server/adam/Adam/Levels/Prime/L02_Prime.lean index 0cc19a3..58231bf 100644 --- a/server/adam/Adam/Levels/Prime/L02_Prime.lean +++ b/server/adam/Adam/Levels/Prime/L02_Prime.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Nat.Prime import Std.Tactic.RCases @@ -9,9 +9,9 @@ import Mathlib.Tactic.Ring -- import Data.Nat.Prime -import TestGame.ToBePorted +import Adam.ToBePorted -Game "TestGame" +Game "Adam" World "Prime" Level 2 diff --git a/server/adam/Adam/Levels/Prime/L03_Prime.lean b/server/adam/Adam/Levels/Prime/L03_Prime.lean index 741bb71..a437d02 100644 --- a/server/adam/Adam/Levels/Prime/L03_Prime.lean +++ b/server/adam/Adam/Levels/Prime/L03_Prime.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Nat.Prime import Std.Tactic.RCases @@ -7,9 +7,9 @@ import Mathlib.Tactic.Contrapose import Mathlib.Tactic.Use import Mathlib.Tactic.Ring -import TestGame.ToBePorted +import Adam.ToBePorted -Game "TestGame" +Game "Adam" World "Prime" Level 3 diff --git a/server/adam/Adam/Levels/Prime/L06_ExistsUnique.lean b/server/adam/Adam/Levels/Prime/L06_ExistsUnique.lean index bd8a3dc..3094ea7 100644 --- a/server/adam/Adam/Levels/Prime/L06_ExistsUnique.lean +++ b/server/adam/Adam/Levels/Prime/L06_ExistsUnique.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Nat.Prime import Std.Tactic.RCases @@ -7,9 +7,9 @@ import Mathlib.Tactic.Contrapose import Mathlib.Tactic.Use import Mathlib.Tactic.Ring -import TestGame.ToBePorted +import Adam.ToBePorted -Game "TestGame" +Game "Adam" World "Prime" Level 4 diff --git a/server/adam/Adam/Levels/Proposition.lean b/server/adam/Adam/Levels/Proposition.lean index bf6ec84..640929b 100644 --- a/server/adam/Adam/Levels/Proposition.lean +++ b/server/adam/Adam/Levels/Proposition.lean @@ -1,19 +1,19 @@ -import TestGame.Levels.Proposition.L00_Tauto -import TestGame.Levels.Proposition.L01_Rfl -import TestGame.Levels.Proposition.L02_Assumption -import TestGame.Levels.Proposition.L03_Assumption -import TestGame.Levels.Proposition.L04_True -import TestGame.Levels.Proposition.L05_Not -import TestGame.Levels.Proposition.L06_False -import TestGame.Levels.Proposition.L07_ContraNotEq -import TestGame.Levels.Proposition.L08_Contra -import TestGame.Levels.Proposition.L09_And -import TestGame.Levels.Proposition.L10_And -import TestGame.Levels.Proposition.L11_Or -import TestGame.Levels.Proposition.L12_Or -import TestGame.Levels.Proposition.L13_Summary +import Adam.Levels.Proposition.L00_Tauto +import Adam.Levels.Proposition.L01_Rfl +import Adam.Levels.Proposition.L02_Assumption +import Adam.Levels.Proposition.L03_Assumption +import Adam.Levels.Proposition.L04_True +import Adam.Levels.Proposition.L05_Not +import Adam.Levels.Proposition.L06_False +import Adam.Levels.Proposition.L07_ContraNotEq +import Adam.Levels.Proposition.L08_Contra +import Adam.Levels.Proposition.L09_And +import Adam.Levels.Proposition.L10_And +import Adam.Levels.Proposition.L11_Or +import Adam.Levels.Proposition.L12_Or +import Adam.Levels.Proposition.L13_Summary -Game "TestGame" +Game "Adam" World "Proposition" Title "Aussagenlogik 1" diff --git a/server/adam/Adam/Levels/Proposition/L00_Tauto.lean b/server/adam/Adam/Levels/Proposition/L00_Tauto.lean index 99204e4..4a7d298 100644 --- a/server/adam/Adam/Levels/Proposition/L00_Tauto.lean +++ b/server/adam/Adam/Levels/Proposition/L00_Tauto.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Tactic.Tauto -Game "TestGame" +Game "Adam" World "Proposition" Level 1 diff --git a/server/adam/Adam/Levels/Proposition/L01_Rfl.lean b/server/adam/Adam/Levels/Proposition/L01_Rfl.lean index 3c56590..984e7f9 100644 --- a/server/adam/Adam/Levels/Proposition/L01_Rfl.lean +++ b/server/adam/Adam/Levels/Proposition/L01_Rfl.lean @@ -1,6 +1,6 @@ -import TestGame.Metadata +import Adam.Metadata -Game "TestGame" +Game "Adam" World "Proposition" Level 2 diff --git a/server/adam/Adam/Levels/Proposition/L02_Assumption.lean b/server/adam/Adam/Levels/Proposition/L02_Assumption.lean index e75e141..e3101cb 100644 --- a/server/adam/Adam/Levels/Proposition/L02_Assumption.lean +++ b/server/adam/Adam/Levels/Proposition/L02_Assumption.lean @@ -1,6 +1,6 @@ -import TestGame.Metadata +import Adam.Metadata -Game "TestGame" +Game "Adam" World "Proposition" Level 3 diff --git a/server/adam/Adam/Levels/Proposition/L03_Assumption.lean b/server/adam/Adam/Levels/Proposition/L03_Assumption.lean index 64cdbb7..f341cbc 100644 --- a/server/adam/Adam/Levels/Proposition/L03_Assumption.lean +++ b/server/adam/Adam/Levels/Proposition/L03_Assumption.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Nat.Basic -- TODO -Game "TestGame" +Game "Adam" World "Proposition" Level 4 diff --git a/server/adam/Adam/Levels/Proposition/L04_True.lean b/server/adam/Adam/Levels/Proposition/L04_True.lean index 0549e7c..2be1ea1 100644 --- a/server/adam/Adam/Levels/Proposition/L04_True.lean +++ b/server/adam/Adam/Levels/Proposition/L04_True.lean @@ -1,6 +1,6 @@ -import TestGame.Metadata +import Adam.Metadata -Game "TestGame" +Game "Adam" World "Proposition" Level 5 diff --git a/server/adam/Adam/Levels/Proposition/L05_Not.lean b/server/adam/Adam/Levels/Proposition/L05_Not.lean index dc1d413..486072f 100644 --- a/server/adam/Adam/Levels/Proposition/L05_Not.lean +++ b/server/adam/Adam/Levels/Proposition/L05_Not.lean @@ -1,6 +1,6 @@ -import TestGame.Metadata +import Adam.Metadata -Game "TestGame" +Game "Adam" World "Proposition" Level 6 diff --git a/server/adam/Adam/Levels/Proposition/L06_False.lean b/server/adam/Adam/Levels/Proposition/L06_False.lean index f60ad4f..16de21d 100644 --- a/server/adam/Adam/Levels/Proposition/L06_False.lean +++ b/server/adam/Adam/Levels/Proposition/L06_False.lean @@ -1,8 +1,8 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.LeftRight -Game "TestGame" +Game "Adam" World "Proposition" Level 7 diff --git a/server/adam/Adam/Levels/Proposition/L07_ContraNotEq.lean b/server/adam/Adam/Levels/Proposition/L07_ContraNotEq.lean index 88900b5..3f46d12 100644 --- a/server/adam/Adam/Levels/Proposition/L07_ContraNotEq.lean +++ b/server/adam/Adam/Levels/Proposition/L07_ContraNotEq.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.LeftRight -import TestGame.ToBePorted +import Adam.ToBePorted -Game "TestGame" +Game "Adam" World "Proposition" Level 8 diff --git a/server/adam/Adam/Levels/Proposition/L08_Contra.lean b/server/adam/Adam/Levels/Proposition/L08_Contra.lean index 6f9a195..86d5e0a 100644 --- a/server/adam/Adam/Levels/Proposition/L08_Contra.lean +++ b/server/adam/Adam/Levels/Proposition/L08_Contra.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.LeftRight -import TestGame.ToBePorted +import Adam.ToBePorted -Game "TestGame" +Game "Adam" World "Proposition" Level 9 diff --git a/server/adam/Adam/Levels/Proposition/L09_And.lean b/server/adam/Adam/Levels/Proposition/L09_And.lean index 5411259..3ba43a8 100644 --- a/server/adam/Adam/Levels/Proposition/L09_And.lean +++ b/server/adam/Adam/Levels/Proposition/L09_And.lean @@ -1,9 +1,9 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Proposition" Level 10 diff --git a/server/adam/Adam/Levels/Proposition/L10_And.lean b/server/adam/Adam/Levels/Proposition/L10_And.lean index 44aad21..3204f4a 100644 --- a/server/adam/Adam/Levels/Proposition/L10_And.lean +++ b/server/adam/Adam/Levels/Proposition/L10_And.lean @@ -1,9 +1,9 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Proposition" Level 11 diff --git a/server/adam/Adam/Levels/Proposition/L11_Or.lean b/server/adam/Adam/Levels/Proposition/L11_Or.lean index 0c5878b..b3642a9 100644 --- a/server/adam/Adam/Levels/Proposition/L11_Or.lean +++ b/server/adam/Adam/Levels/Proposition/L11_Or.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.LeftRight --set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Proposition" Level 12 diff --git a/server/adam/Adam/Levels/Proposition/L12_Or.lean b/server/adam/Adam/Levels/Proposition/L12_Or.lean index 90aa1b1..8c6959c 100644 --- a/server/adam/Adam/Levels/Proposition/L12_Or.lean +++ b/server/adam/Adam/Levels/Proposition/L12_Or.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.LeftRight @@ -7,7 +7,7 @@ set_option tactic.hygienic false --set_option autoImplicit false -Game "TestGame" +Game "Adam" World "Proposition" Level 13 diff --git a/server/adam/Adam/Levels/Proposition/L13_Summary.lean b/server/adam/Adam/Levels/Proposition/L13_Summary.lean index 6db6c77..8d4c151 100644 --- a/server/adam/Adam/Levels/Proposition/L13_Summary.lean +++ b/server/adam/Adam/Levels/Proposition/L13_Summary.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Std.Tactic.RCases import Mathlib.Tactic.LeftRight set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Proposition" Level 14 diff --git a/server/adam/Adam/Levels/SetFunction.lean b/server/adam/Adam/Levels/SetFunction.lean index bf9cfbc..a6f2b4b 100644 --- a/server/adam/Adam/Levels/SetFunction.lean +++ b/server/adam/Adam/Levels/SetFunction.lean @@ -1,8 +1,8 @@ -import TestGame.Levels.SetFunction.L01_Image -import TestGame.Levels.SetFunction.L02_Preimage -import TestGame.Levels.SetFunction.L03_Range -import TestGame.Levels.SetFunction.L04_ImageUnion +import Adam.Levels.SetFunction.L01_Image +import Adam.Levels.SetFunction.L02_Preimage +import Adam.Levels.SetFunction.L03_Range +import Adam.Levels.SetFunction.L04_ImageUnion -Game "TestGame" +Game "Adam" World "SetFunction" Title "Abbildungen 2" diff --git a/server/adam/Adam/Levels/SetFunction/L01_Image.lean b/server/adam/Adam/Levels/SetFunction/L01_Image.lean index 1bfede9..9d0dbd6 100644 --- a/server/adam/Adam/Levels/SetFunction/L01_Image.lean +++ b/server/adam/Adam/Levels/SetFunction/L01_Image.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -Game "TestGame" +Game "Adam" World "SetFunction" Level 1 diff --git a/server/adam/Adam/Levels/SetFunction/L02_Preimage.lean b/server/adam/Adam/Levels/SetFunction/L02_Preimage.lean index b94e605..4f37c77 100644 --- a/server/adam/Adam/Levels/SetFunction/L02_Preimage.lean +++ b/server/adam/Adam/Levels/SetFunction/L02_Preimage.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -Game "TestGame" +Game "Adam" World "SetFunction" Level 2 diff --git a/server/adam/Adam/Levels/SetFunction/L03_Range.lean b/server/adam/Adam/Levels/SetFunction/L03_Range.lean index 21d2ccc..4809e8f 100644 --- a/server/adam/Adam/Levels/SetFunction/L03_Range.lean +++ b/server/adam/Adam/Levels/SetFunction/L03_Range.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -Game "TestGame" +Game "Adam" World "SetFunction" Level 3 diff --git a/server/adam/Adam/Levels/SetFunction/L04_ImageUnion.lean b/server/adam/Adam/Levels/SetFunction/L04_ImageUnion.lean index 7bfcfca..ccf1c7a 100644 --- a/server/adam/Adam/Levels/SetFunction/L04_ImageUnion.lean +++ b/server/adam/Adam/Levels/SetFunction/L04_ImageUnion.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -Game "TestGame" +Game "Adam" World "SetFunction" Level 4 diff --git a/server/adam/Adam/Levels/SetTheory.lean b/server/adam/Adam/Levels/SetTheory.lean index 298c096..59ca233 100644 --- a/server/adam/Adam/Levels/SetTheory.lean +++ b/server/adam/Adam/Levels/SetTheory.lean @@ -1,25 +1,25 @@ -import TestGame.Levels.SetTheory.L01_Univ -import TestGame.Levels.SetTheory.L02_Empty -import TestGame.Levels.SetTheory.L03_Subset -import TestGame.Levels.SetTheory.L04_SubsetEmpty -import TestGame.Levels.SetTheory.L05_Empty -import TestGame.Levels.SetTheory.L06_Nonempty -import TestGame.Levels.SetTheory.L07_UnionInter -import TestGame.Levels.SetTheory.L08_UnionInter -import TestGame.Levels.SetTheory.L09_Complement -import TestGame.Levels.SetTheory.L10_Morgan -import TestGame.Levels.SetTheory.L11_SSubset -import TestGame.Levels.SetTheory.L12_Insert -import TestGame.Levels.SetTheory.L13_Insert -import TestGame.Levels.SetTheory.L14_SetOf -import TestGame.Levels.SetTheory.L15_Powerset -import TestGame.Levels.SetTheory.L16_Disjoint -import TestGame.Levels.SetTheory.L17_SetOf -import TestGame.Levels.SetTheory.L18_SetOf -import TestGame.Levels.SetTheory.L19_Subtype - - -Game "TestGame" +import Adam.Levels.SetTheory.L01_Univ +import Adam.Levels.SetTheory.L02_Empty +import Adam.Levels.SetTheory.L03_Subset +import Adam.Levels.SetTheory.L04_SubsetEmpty +import Adam.Levels.SetTheory.L05_Empty +import Adam.Levels.SetTheory.L06_Nonempty +import Adam.Levels.SetTheory.L07_UnionInter +import Adam.Levels.SetTheory.L08_UnionInter +import Adam.Levels.SetTheory.L09_Complement +import Adam.Levels.SetTheory.L10_Morgan +import Adam.Levels.SetTheory.L11_SSubset +import Adam.Levels.SetTheory.L12_Insert +import Adam.Levels.SetTheory.L13_Insert +import Adam.Levels.SetTheory.L14_SetOf +import Adam.Levels.SetTheory.L15_Powerset +import Adam.Levels.SetTheory.L16_Disjoint +import Adam.Levels.SetTheory.L17_SetOf +import Adam.Levels.SetTheory.L18_SetOf +import Adam.Levels.SetTheory.L19_Subtype + + +Game "Adam" World "SetTheory" Title "Mengenlehre" @@ -38,6 +38,6 @@ Sofort begrüßt euch eine ältere Frau, die sich als *Mengea*, die Beschützeri vorstellt. " -Game "TestGame" +Game "Adam" World "SetTheory2" Title "Mehr Mengenlehre" diff --git a/server/adam/Adam/Levels/SetTheory/L01_Univ.lean b/server/adam/Adam/Levels/SetTheory/L01_Univ.lean index 8e67b91..f192095 100644 --- a/server/adam/Adam/Levels/SetTheory/L01_Univ.lean +++ b/server/adam/Adam/Levels/SetTheory/L01_Univ.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Init.Set import Mathlib.Tactic.Tauto @@ -6,7 +6,7 @@ import Mathlib.Tactic.Tauto set_option tactic.hygienic false set_option autoImplicit false -Game "TestGame" +Game "Adam" World "SetTheory" Level 1 diff --git a/server/adam/Adam/Levels/SetTheory/L02_Empty.lean b/server/adam/Adam/Levels/SetTheory/L02_Empty.lean index 57681d9..1840659 100644 --- a/server/adam/Adam/Levels/SetTheory/L02_Empty.lean +++ b/server/adam/Adam/Levels/SetTheory/L02_Empty.lean @@ -1,11 +1,11 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Init.Set import Mathlib.Tactic.Tauto set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "SetTheory" Level 2 diff --git a/server/adam/Adam/Levels/SetTheory/L03_Subset.lean b/server/adam/Adam/Levels/SetTheory/L03_Subset.lean index 17f9af6..f87406a 100644 --- a/server/adam/Adam/Levels/SetTheory/L03_Subset.lean +++ b/server/adam/Adam/Levels/SetTheory/L03_Subset.lean @@ -1,11 +1,11 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Init.Set import Mathlib.Tactic.Tauto set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "SetTheory" Level 3 diff --git a/server/adam/Adam/Levels/SetTheory/L04_SubsetEmpty.lean b/server/adam/Adam/Levels/SetTheory/L04_SubsetEmpty.lean index 4ef1bd8..9889ea6 100644 --- a/server/adam/Adam/Levels/SetTheory/L04_SubsetEmpty.lean +++ b/server/adam/Adam/Levels/SetTheory/L04_SubsetEmpty.lean @@ -1,5 +1,5 @@ -import TestGame.Metadata -import TestGame.Levels.SetTheory.L03_Subset +import Adam.Metadata +import Adam.Levels.SetTheory.L03_Subset import Mathlib.Init.Set import Mathlib.Tactic.Tauto @@ -7,7 +7,7 @@ import Mathlib set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "SetTheory" Level 4 diff --git a/server/adam/Adam/Levels/SetTheory/L05_Empty.lean b/server/adam/Adam/Levels/SetTheory/L05_Empty.lean index fc4e714..f284019 100644 --- a/server/adam/Adam/Levels/SetTheory/L05_Empty.lean +++ b/server/adam/Adam/Levels/SetTheory/L05_Empty.lean @@ -1,5 +1,5 @@ -import TestGame.Metadata -import TestGame.Levels.SetTheory.L04_SubsetEmpty +import Adam.Metadata +import Adam.Levels.SetTheory.L04_SubsetEmpty --import Mathlib.Data.Set.Basic import Mathlib.Init.Set @@ -8,7 +8,7 @@ import Mathlib.Tactic.PushNeg set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "SetTheory" Level 5 diff --git a/server/adam/Adam/Levels/SetTheory/L06_Nonempty.lean b/server/adam/Adam/Levels/SetTheory/L06_Nonempty.lean index b3adf6e..a55b084 100644 --- a/server/adam/Adam/Levels/SetTheory/L06_Nonempty.lean +++ b/server/adam/Adam/Levels/SetTheory/L06_Nonempty.lean @@ -1,11 +1,11 @@ -import TestGame.Metadata -import TestGame.Levels.SetTheory.L05_Empty +import Adam.Metadata +import Adam.Levels.SetTheory.L05_Empty import Mathlib.Data.Set.Basic set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "SetTheory" Level 6 diff --git a/server/adam/Adam/Levels/SetTheory/L07_UnionInter.lean b/server/adam/Adam/Levels/SetTheory/L07_UnionInter.lean index cbb767b..31f8c1d 100644 --- a/server/adam/Adam/Levels/SetTheory/L07_UnionInter.lean +++ b/server/adam/Adam/Levels/SetTheory/L07_UnionInter.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Set.Basic set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "SetTheory" Level 7 diff --git a/server/adam/Adam/Levels/SetTheory/L08_UnionInter.lean b/server/adam/Adam/Levels/SetTheory/L08_UnionInter.lean index 8da2a5a..072434b 100644 --- a/server/adam/Adam/Levels/SetTheory/L08_UnionInter.lean +++ b/server/adam/Adam/Levels/SetTheory/L08_UnionInter.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Set.Basic set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "SetTheory" Level 8 diff --git a/server/adam/Adam/Levels/SetTheory/L09_Complement.lean b/server/adam/Adam/Levels/SetTheory/L09_Complement.lean index f9481bf..0635df4 100644 --- a/server/adam/Adam/Levels/SetTheory/L09_Complement.lean +++ b/server/adam/Adam/Levels/SetTheory/L09_Complement.lean @@ -1,8 +1,8 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Set.Basic -Game "TestGame" +Game "Adam" World "SetTheory" Level 9 diff --git a/server/adam/Adam/Levels/SetTheory/L10_Morgan.lean b/server/adam/Adam/Levels/SetTheory/L10_Morgan.lean index 76b6900..db12481 100644 --- a/server/adam/Adam/Levels/SetTheory/L10_Morgan.lean +++ b/server/adam/Adam/Levels/SetTheory/L10_Morgan.lean @@ -1,8 +1,8 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Set.Basic -Game "TestGame" +Game "Adam" World "SetTheory" Level 10 diff --git a/server/adam/Adam/Levels/SetTheory/L11_SSubset.lean b/server/adam/Adam/Levels/SetTheory/L11_SSubset.lean index fbcf31c..e587290 100644 --- a/server/adam/Adam/Levels/SetTheory/L11_SSubset.lean +++ b/server/adam/Adam/Levels/SetTheory/L11_SSubset.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Set.Basic -Game "TestGame" +Game "Adam" World "SetTheory" Level 11 diff --git a/server/adam/Adam/Levels/SetTheory/L12_Insert.lean b/server/adam/Adam/Levels/SetTheory/L12_Insert.lean index 23f484f..6996503 100644 --- a/server/adam/Adam/Levels/SetTheory/L12_Insert.lean +++ b/server/adam/Adam/Levels/SetTheory/L12_Insert.lean @@ -1,8 +1,8 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Set.Basic -Game "TestGame" +Game "Adam" World "SetTheory" Level 12 diff --git a/server/adam/Adam/Levels/SetTheory/L13_Insert.lean b/server/adam/Adam/Levels/SetTheory/L13_Insert.lean index cb32a1a..30ab7d8 100644 --- a/server/adam/Adam/Levels/SetTheory/L13_Insert.lean +++ b/server/adam/Adam/Levels/SetTheory/L13_Insert.lean @@ -1,8 +1,8 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Set.Basic -Game "TestGame" +Game "Adam" World "SetTheory" Level 13 diff --git a/server/adam/Adam/Levels/SetTheory/L14_SetOf.lean b/server/adam/Adam/Levels/SetTheory/L14_SetOf.lean index f87e21b..e0fcc3c 100644 --- a/server/adam/Adam/Levels/SetTheory/L14_SetOf.lean +++ b/server/adam/Adam/Levels/SetTheory/L14_SetOf.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Set.Basic import Mathlib.Algebra.Parity import Mathlib.Tactic.Ring -Game "TestGame" +Game "Adam" World "SetTheory2" Level 1 diff --git a/server/adam/Adam/Levels/SetTheory/L15_Powerset.lean b/server/adam/Adam/Levels/SetTheory/L15_Powerset.lean index c2fbe30..9c8acc9 100644 --- a/server/adam/Adam/Levels/SetTheory/L15_Powerset.lean +++ b/server/adam/Adam/Levels/SetTheory/L15_Powerset.lean @@ -1,12 +1,12 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Set.Basic import Mathlib.Algebra.Parity import Mathlib.Tactic.Ring -import TestGame.ToBePorted +import Adam.ToBePorted -Game "TestGame" +Game "Adam" World "SetTheory2" Level 2 diff --git a/server/adam/Adam/Levels/SetTheory/L16_Disjoint.lean b/server/adam/Adam/Levels/SetTheory/L16_Disjoint.lean index 606947f..5cf6745 100644 --- a/server/adam/Adam/Levels/SetTheory/L16_Disjoint.lean +++ b/server/adam/Adam/Levels/SetTheory/L16_Disjoint.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib import Mathlib.Algebra.Parity import Mathlib.Tactic.Ring -Game "TestGame" +Game "Adam" World "SetTheory2" Level 3 diff --git a/server/adam/Adam/Levels/SetTheory/L17_SetOf.lean b/server/adam/Adam/Levels/SetTheory/L17_SetOf.lean index 975846f..80b1bb2 100644 --- a/server/adam/Adam/Levels/SetTheory/L17_SetOf.lean +++ b/server/adam/Adam/Levels/SetTheory/L17_SetOf.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Set.Basic import Mathlib.Algebra.Parity import Mathlib -Game "TestGame" +Game "Adam" World "SetTheory2" Level 4 diff --git a/server/adam/Adam/Levels/SetTheory/L18_SetOf.lean b/server/adam/Adam/Levels/SetTheory/L18_SetOf.lean index d138956..211ec53 100644 --- a/server/adam/Adam/Levels/SetTheory/L18_SetOf.lean +++ b/server/adam/Adam/Levels/SetTheory/L18_SetOf.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Set.Basic import Mathlib.Algebra.Parity import Mathlib -Game "TestGame" +Game "Adam" World "SetTheory2" Level 5 diff --git a/server/adam/Adam/Levels/SetTheory/L19_Subtype.lean b/server/adam/Adam/Levels/SetTheory/L19_Subtype.lean index 61abddd..20d82c2 100644 --- a/server/adam/Adam/Levels/SetTheory/L19_Subtype.lean +++ b/server/adam/Adam/Levels/SetTheory/L19_Subtype.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Set.Basic import Mathlib.Algebra.Parity import Mathlib.Tactic.Ring -Game "TestGame" +Game "Adam" World "SetTheory2" Level 6 diff --git a/server/adam/Adam/Levels/SetTheory/L20_UnionInter.lean b/server/adam/Adam/Levels/SetTheory/L20_UnionInter.lean index c61c6ab..132da70 100644 --- a/server/adam/Adam/Levels/SetTheory/L20_UnionInter.lean +++ b/server/adam/Adam/Levels/SetTheory/L20_UnionInter.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Set.Basic import Mathlib.Algebra.Parity import Mathlib -Game "TestGame" +Game "Adam" World "SetTheory2" Level 7 diff --git a/server/adam/Adam/Levels/SetTheory/L21_Summary.lean b/server/adam/Adam/Levels/SetTheory/L21_Summary.lean index 1e45403..83e645c 100644 --- a/server/adam/Adam/Levels/SetTheory/L21_Summary.lean +++ b/server/adam/Adam/Levels/SetTheory/L21_Summary.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Data.Set.Basic import Mathlib.Algebra.Parity import Mathlib.Tactic.Ring -Game "TestGame" +Game "Adam" World "SetTheory" Level 21 diff --git a/server/adam/Adam/Levels/SetTheory/T01_Set.lean b/server/adam/Adam/Levels/SetTheory/T01_Set.lean index f8ac55d..21e9d0b 100644 --- a/server/adam/Adam/Levels/SetTheory/T01_Set.lean +++ b/server/adam/Adam/Levels/SetTheory/T01_Set.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Order.SymmDiff import Mathlib.Logic.Function.Iterate @@ -14,7 +14,7 @@ import Mathlib set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "SetTheory" Level 1 diff --git a/server/adam/Adam/Levels/SetTheory/T04_xx.lean b/server/adam/Adam/Levels/SetTheory/T04_xx.lean index bb8523c..7d0f0ad 100644 --- a/server/adam/Adam/Levels/SetTheory/T04_xx.lean +++ b/server/adam/Adam/Levels/SetTheory/T04_xx.lean @@ -1,4 +1,4 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib import Duper.Tactic @@ -8,7 +8,7 @@ import Mathlib.Order.Disjoint set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "SetTheory" Level 4 diff --git a/server/adam/Adam/Levels/StatementTest.lean b/server/adam/Adam/Levels/StatementTest.lean index 2d00bb9..db6bc7f 100644 --- a/server/adam/Adam/Levels/StatementTest.lean +++ b/server/adam/Adam/Levels/StatementTest.lean @@ -1,7 +1,7 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib -Game "TestGame" +Game "Adam" World "TestWorld" Level 1 diff --git a/server/adam/Adam/Levels/Sum.lean b/server/adam/Adam/Levels/Sum.lean index 74c3fd7..5f5172b 100644 --- a/server/adam/Adam/Levels/Sum.lean +++ b/server/adam/Adam/Levels/Sum.lean @@ -1,11 +1,11 @@ -import TestGame.Levels.Sum.L01_Simp -import TestGame.Levels.Sum.L02_Sum -import TestGame.Levels.Sum.L03_ArithSum -import TestGame.Levels.Sum.L04_SumOdd -import TestGame.Levels.Sum.L05_SumComm -import TestGame.Levels.Sum.L06_Summary +import Adam.Levels.Sum.L01_Simp +import Adam.Levels.Sum.L02_Sum +import Adam.Levels.Sum.L03_ArithSum +import Adam.Levels.Sum.L04_SumOdd +import Adam.Levels.Sum.L05_SumComm +import Adam.Levels.Sum.L06_Summary -Game "TestGame" +Game "Adam" World "Sum" Title "Endliche Summe" diff --git a/server/adam/Adam/Levels/Sum/L01_Simp.lean b/server/adam/Adam/Levels/Sum/L01_Simp.lean index ec2c5c4..a735024 100644 --- a/server/adam/Adam/Levels/Sum/L01_Simp.lean +++ b/server/adam/Adam/Levels/Sum/L01_Simp.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata -import TestGame.ToBePorted +import Adam.ToBePorted set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Sum" Level 1 diff --git a/server/adam/Adam/Levels/Sum/L02_Sum.lean b/server/adam/Adam/Levels/Sum/L02_Sum.lean index 039c2b7..65a3ad0 100644 --- a/server/adam/Adam/Levels/Sum/L02_Sum.lean +++ b/server/adam/Adam/Levels/Sum/L02_Sum.lean @@ -1,11 +1,11 @@ -import TestGame.Metadata +import Adam.Metadata -import TestGame.ToBePorted +import Adam.ToBePorted import Mathlib set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Sum" Level 2 diff --git a/server/adam/Adam/Levels/Sum/L03_ArithSum.lean b/server/adam/Adam/Levels/Sum/L03_ArithSum.lean index 526b720..c87d95e 100644 --- a/server/adam/Adam/Levels/Sum/L03_ArithSum.lean +++ b/server/adam/Adam/Levels/Sum/L03_ArithSum.lean @@ -1,13 +1,13 @@ -import TestGame.Metadata +import Adam.Metadata import Mathlib.Algebra.BigOperators.Fin import Mathlib.Tactic.Ring -import TestGame.ToBePorted +import Adam.ToBePorted set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Sum" Level 3 diff --git a/server/adam/Adam/Levels/Sum/L04_SumOdd.lean b/server/adam/Adam/Levels/Sum/L04_SumOdd.lean index da9b27a..d84dd40 100644 --- a/server/adam/Adam/Levels/Sum/L04_SumOdd.lean +++ b/server/adam/Adam/Levels/Sum/L04_SumOdd.lean @@ -1,10 +1,10 @@ -import TestGame.Metadata +import Adam.Metadata -import TestGame.ToBePorted +import Adam.ToBePorted import Mathlib.Algebra.BigOperators.Fin import Mathlib.Tactic.Ring -Game "TestGame" +Game "Adam" World "Sum" Level 4 diff --git a/server/adam/Adam/Levels/Sum/L05_SumComm.lean b/server/adam/Adam/Levels/Sum/L05_SumComm.lean index b6f8d62..dd5cc37 100644 --- a/server/adam/Adam/Levels/Sum/L05_SumComm.lean +++ b/server/adam/Adam/Levels/Sum/L05_SumComm.lean @@ -1,16 +1,16 @@ -import TestGame.Metadata +import Adam.Metadata -import TestGame.ToBePorted +import Adam.ToBePorted import Mathlib.Algebra.BigOperators.Fin import Mathlib.Tactic.Ring -import TestGame.Options.ArithSum +import Adam.Options.ArithSum set_option tactic.hygienic false open BigOperators -Game "TestGame" +Game "Adam" World "Sum" Level 5 diff --git a/server/adam/Adam/Levels/Sum/L06_Summary.lean b/server/adam/Adam/Levels/Sum/L06_Summary.lean index 6aea6a2..45f2a13 100644 --- a/server/adam/Adam/Levels/Sum/L06_Summary.lean +++ b/server/adam/Adam/Levels/Sum/L06_Summary.lean @@ -1,13 +1,13 @@ -import TestGame.Metadata +import Adam.Metadata -import TestGame.ToBePorted +import Adam.ToBePorted import Mathlib.Algebra.BigOperators.Fin import Mathlib.Tactic.Ring -import TestGame.ToBePorted -import TestGame.Options.ArithSum +import Adam.ToBePorted +import Adam.Options.ArithSum -Game "TestGame" +Game "Adam" World "Sum" Level 6 diff --git a/server/adam/Adam/Levels/Sum/T01_Induction.lean b/server/adam/Adam/Levels/Sum/T01_Induction.lean index b65d4c5..24062ab 100644 --- a/server/adam/Adam/Levels/Sum/T01_Induction.lean +++ b/server/adam/Adam/Levels/Sum/T01_Induction.lean @@ -1,13 +1,13 @@ -import TestGame.Metadata +import Adam.Metadata -import TestGame.ToBePorted +import Adam.ToBePorted import Mathlib.Algebra.BigOperators.Fin set_option tactic.hygienic false open Nat -Game "TestGame" +Game "Adam" World "Sum" Level 2 diff --git a/server/adam/Adam/Levels/Sum/T02_Induction.lean b/server/adam/Adam/Levels/Sum/T02_Induction.lean index 42df47d..09f6400 100644 --- a/server/adam/Adam/Levels/Sum/T02_Induction.lean +++ b/server/adam/Adam/Levels/Sum/T02_Induction.lean @@ -1,11 +1,11 @@ -import TestGame.Metadata +import Adam.Metadata -import TestGame.ToBePorted +import Adam.ToBePorted import Mathlib.Algebra.BigOperators.Fin set_option tactic.hygienic false -Game "TestGame" +Game "Adam" World "Sum" Level 2 diff --git a/server/adam/Adam/Levels/Sum/T03__Bernoulli.lean b/server/adam/Adam/Levels/Sum/T03__Bernoulli.lean index 85c2807..0c73287 100644 --- a/server/adam/Adam/Levels/Sum/T03__Bernoulli.lean +++ b/server/adam/Adam/Levels/Sum/T03__Bernoulli.lean @@ -1,12 +1,12 @@ -import TestGame.Metadata +import Adam.Metadata -import TestGame.ToBePorted +import Adam.ToBePorted import Mathlib.Algebra.BigOperators.Fin import Mathlib.Tactic.Ring -import TestGame.ToBePorted +import Adam.ToBePorted -Game "TestGame" +Game "Adam" World "Sum" Level 5 diff --git a/server/adam/Adam/Metadata.lean b/server/adam/Adam/Metadata.lean index a9fd86a..e0f2b52 100644 --- a/server/adam/Adam/Metadata.lean +++ b/server/adam/Adam/Metadata.lean @@ -1,4 +1,4 @@ import GameServer.Commands -import TestGame.TacticDocs -import TestGame.LemmaDocs +import Adam.TacticDocs +import Adam.LemmaDocs import Mathlib.Init.Data.Nat.Basic -- Imports the notation ℕ. diff --git a/server/adam/Adam/StructInstWithHolesTest.lean b/server/adam/Adam/StructInstWithHolesTest.lean index fe0436c..12fdc8d 100644 --- a/server/adam/Adam/StructInstWithHolesTest.lean +++ b/server/adam/Adam/StructInstWithHolesTest.lean @@ -1,4 +1,4 @@ -import TestGame.StructInstWithHoles +import Adam.StructInstWithHoles import Mathlib diff --git a/server/adam/Adam/TacticDocs.lean b/server/adam/Adam/TacticDocs.lean index 49d56b8..6a3b96d 100644 --- a/server/adam/Adam/TacticDocs.lean +++ b/server/adam/Adam/TacticDocs.lean @@ -1,5 +1,5 @@ import GameServer.Commands -import TestGame.Tactics +import Adam.Tactics TacticDoc assumption " diff --git a/server/adam/Adam/Tactics.lean b/server/adam/Adam/Tactics.lean index 5e95bfc..d5dfd4b 100644 --- a/server/adam/Adam/Tactics.lean +++ b/server/adam/Adam/Tactics.lean @@ -1,5 +1,5 @@ import Lean --- import TestGame.MyNat +-- import Adam.MyNat open Lean Elab Tactic diff --git a/server/adam/lakefile.lean b/server/adam/lakefile.lean index 9ea11dc..d33792a 100644 --- a/server/adam/lakefile.lean +++ b/server/adam/lakefile.lean @@ -6,9 +6,9 @@ require GameServer from ".."/"leanserver" require mathlib from git "https://github.com/leanprover-community/mathlib4.git"@"master" -package TestGame +package Adam @[default_target] -lean_lib TestGame { +lean_lib Adam { moreLeanArgs := #["-DautoImplicit=false"] } diff --git a/server/build.sh b/server/build.sh index 3b85690..21941ea 100755 --- a/server/build.sh +++ b/server/build.sh @@ -6,12 +6,12 @@ cd $(dirname $0) # Build elan image if not already present docker build --pull --rm -f elan.Dockerfile -t elan:latest . -# Build testgame -(cd testgame && lake exe cache get && lake build) -docker rmi testgame:latest || true +# Build adam +(cd adam && lake exe cache get && lake build) +docker rmi adam:latest || true docker build \ - --build-arg GAME_DIR=testgame \ - --rm -f server.Dockerfile -t testgame:latest . + --build-arg GAME_DIR=adam \ + --rm -f server.Dockerfile -t adam:latest . # Build NNG (cd nng && lake build) diff --git a/server/index.mjs b/server/index.mjs index 756987c..cdb6db9 100644 --- a/server/index.mjs +++ b/server/index.mjs @@ -7,9 +7,9 @@ import * as rpc from 'vscode-ws-jsonrpc'; import * as jsonrpcserver from 'vscode-ws-jsonrpc/server'; const games = { - testgame: { - name: "TestGame", - module: "TestGame", + adam: { + name: "Adam", + module: "Adam", queueLength: 5 }, nng: { diff --git a/server/server.Dockerfile b/server/server.Dockerfile index 304b16b..7cf6aee 100644 --- a/server/server.Dockerfile +++ b/server/server.Dockerfile @@ -6,7 +6,7 @@ WORKDIR / # Copy lean files COPY leanserver ./leanserver COPY $GAME_DIR ./$GAME_DIR -# TODO: make `testgame` a build argument +# TODO: make `adam` a build argument WORKDIR /leanserver RUN rm -f ./build/bin/gameserver