From d7effb37533fadabf4bd1e93830bdaa2de4812af Mon Sep 17 00:00:00 2001
From: Marius Kern <mariusskern@gmail.com>
Date: Thu, 20 Jun 2024 17:48:07 +0200
Subject: [PATCH] Moved types to MetaTheories

---
 source/DefaultSituationSpace.mmt |  4 --
 source/MetaTheories.mmt          | 67 +++++++++++++++++++++++---------
 source/Scrolls/CircleType.mmt    | 12 ------
 source/Scrolls/CuboidType.mmt    | 11 ------
 source/Scrolls/SphereScroll.mmt  | 11 ------
 5 files changed, 49 insertions(+), 56 deletions(-)
 delete mode 100644 source/Scrolls/CircleType.mmt
 delete mode 100644 source/Scrolls/CuboidType.mmt

diff --git a/source/DefaultSituationSpace.mmt b/source/DefaultSituationSpace.mmt
index 254e098..7be9ac6 100644
--- a/source/DefaultSituationSpace.mmt
+++ b/source/DefaultSituationSpace.mmt
@@ -30,9 +30,5 @@ theory DefaultSituationSpace =
         include ?TriangleScroll ❙
         include ?SimpleCircleScroll ❙
         include ?SphereScroll ❙
-        
-
-
-
     ❚
 ❚
diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt
index 2a9f201..aedd54d 100644
--- a/source/MetaTheories.mmt
+++ b/source/MetaTheories.mmt
@@ -318,6 +318,44 @@ theory FrameITCylinder =
 
  ❚
 
+theory CircleType =
+  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+  include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
+  include ?FrameITBasics ❙
+
+  circleType : type ❘ # Circle ❙
+  circleCons : point ⟶ point ⟶ point  ⟶ Circle  ❘ # CircleCons 1 2 3 ❙
+❚
+
+theory SphereType =
+  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+  include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
+  include ?FrameITBasics ❙
+
+  sphereType : type ❘ # Sphere ❙
+  sphereCons : point ⟶ point  ⟶ Sphere  ❘ # SphereCons 1 2 ❙
+  
+❚
+
+theory RectangleType =
+  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+  include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
+  include ?FrameITBasics ❙
+
+  rectangleType : type ❘ # Rectangle ❙
+  rectangleCons : point ⟶ point ⟶ point  ⟶ Rectangle  ❘ # RectangleCons 1 2 3 ❙
+❚
+
+theory CuboidType =
+  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+  include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
+  include ?FrameITBasics ❙
+  include ?RectangleType ❙
+
+  cuboidType : type ❘ # Cuboid ❙
+  cuboidCons : Rectangle ⟶ point ⟶ Cuboid ❘ # CuboidCons 1 2 ❙
+❚
+
 theory FrameITTheories =
   include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
   include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
@@ -326,32 +364,25 @@ theory FrameITTheories =
   include ?FrameITCircle ❙
   include ?FrameITCone ❙
   include ?FrameITCylinder ❙
+  include ?CircleType ❙
+  include ?SphereType ❙
+  include ?RectangleType ❙
+  include ?CuboidType ❙
 
-      makeCircleOf3EdgePoints : point ⟶ point ⟶ point ⟶ circle  ❘ = [p1,p2,p3 ] mkCirc3D (  Ppara p1 (p2 p-p p1) ( p3 p-p p1) ) ( midTriangle3D ( Δ p1 p2 p3 ) ) ( d- ( midTriangle3D ( Δ p1 p2 p3 ) ) p1 )   ❘ # mkCirc3P3D 1 2 3 ❙
-
-   ❚
+  makeCircleOf3EdgePoints : point ⟶ point ⟶ point ⟶ circle  ❘ = [p1,p2,p3 ] mkCirc3D (  Ppara p1 (p2 p-p p1) ( p3 p-p p1) ) ( midTriangle3D ( Δ p1 p2 p3 ) ) ( d- ( midTriangle3D ( Δ p1 p2 p3 ) ) p1 )   ❘ # mkCirc3P3D 1 2 3 ❙
+❚
 
 /T The meta theory to use for situation theories, scroll problem, and scroll solution theories ❚
 theory FrameworldMeta =
   include ?MetaAnnotations ❙
   include ?FrameITTheories ❙
-  include ?RectangleType ❙
-  include ?CuboidType ❙
-  include ?CircleType ❙
-  include ?SphereType ❙
-
- // include ☞http://mathhub.info/MitM/core/arithmetics?RealArithmetics ❙
 
+  // include ☞http://mathhub.info/MitM/core/arithmetics?RealArithmetics ❙
+  // include ☞http://gl.mathhub.info/MMT/LFX/Sigma?LFSigma ❙
+  // include ☞http://mathhub.info/MitM/Foundation?Strings ❙
 
- // include ☞http://gl.mathhub.info/MMT/LFX/Sigma?LFSigma ❙
-
-//  include ☞http://mathhub.info/MitM/Foundation?Strings ❙
   include ☞http://mathhub.info/MitM/Foundation?Math ❙
 
-
-//  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
-//  include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
-
-
-
+  // include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+  // include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
 ❚
diff --git a/source/Scrolls/CircleType.mmt b/source/Scrolls/CircleType.mmt
deleted file mode 100644
index 2fda840..0000000
--- a/source/Scrolls/CircleType.mmt
+++ /dev/null
@@ -1,12 +0,0 @@
-namespace http://mathhub.info/FrameIT/frameworld ❚
-fixmeta ?FrameworldMeta ❚
-
-theory CircleType =
-  
-  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
-  include ?FrameITBasics ❙
-
-  circleType : type ❘ # Circle ❙
-  circleCons : point ⟶ point ⟶ point  ⟶ Circle  ❘ # CircleCons 1 2 3 ❙
-  
-❚
\ No newline at end of file
diff --git a/source/Scrolls/CuboidType.mmt b/source/Scrolls/CuboidType.mmt
deleted file mode 100644
index 8f5f066..0000000
--- a/source/Scrolls/CuboidType.mmt
+++ /dev/null
@@ -1,11 +0,0 @@
-namespace http://mathhub.info/FrameIT/frameworld ❚
-fixmeta ur:?LF ❚
-
-theory CuboidType =
-    include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
-    include ?FrameITBasics ❙
-    include ?RectangleType ❙
-
-    cuboidType : type ❘ # Cuboid ❙
-    cuboidCons : Rectangle ⟶ point ⟶ Cuboid ❘ # CuboidCons 1 2 ❙
-❚
\ No newline at end of file
diff --git a/source/Scrolls/SphereScroll.mmt b/source/Scrolls/SphereScroll.mmt
index ceb193e..858a469 100644
--- a/source/Scrolls/SphereScroll.mmt
+++ b/source/Scrolls/SphereScroll.mmt
@@ -1,17 +1,6 @@
 namespace http://mathhub.info/FrameIT/frameworld ❚
 fixmeta ?FrameworldMeta ❚
 
-theory SphereType =
-  
-  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
-  include ?FrameITBasics ❙
-
-  sphereType : type ❘ # Sphere ❙
-  sphereCons : point ⟶ point  ⟶ Sphere  ❘ # SphereCons 1 2 ❙
-  
-❚
-
-
 theory SphereScroll =
     meta ?MetaAnnotations?problemTheory  ?SphereScroll/Problem ❙
     meta ?MetaAnnotations?solutionTheory ?SphereScroll/Solution ❙
-- 
GitLab