From d3abe71acf6f67fa8af9fd5e980ed31cdfe1c7a4 Mon Sep 17 00:00:00 2001
From: Marius Kern <mariusskern@gmail.com>
Date: Fri, 2 Aug 2024 15:10:27 +0200
Subject: [PATCH] Pyramid added

---
 source/DefaultSituationSpace.mmt |  1 +
 source/MetaTheories.mmt          | 10 ++++++++++
 source/Scrolls/PyramidScroll.mmt | 31 +++++++++++++++++++++++++++++++
 3 files changed, 42 insertions(+)
 create mode 100644 source/Scrolls/PyramidScroll.mmt

diff --git a/source/DefaultSituationSpace.mmt b/source/DefaultSituationSpace.mmt
index 29994d4..b6b42f4 100644
--- a/source/DefaultSituationSpace.mmt
+++ b/source/DefaultSituationSpace.mmt
@@ -29,6 +29,7 @@ theory DefaultSituationSpace =
         include ?CuboidScroll ❙
         include ?TriangleScroll ❙
         include ?PrismScroll ❙
+        include ?PyramidScroll ❙
         include ?SimpleCircleScroll ❙
         include ?SphereScroll ❙
         include ?CylinderScroll ❙
diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt
index c405bff..98311f4 100644
--- a/source/MetaTheories.mmt
+++ b/source/MetaTheories.mmt
@@ -373,6 +373,15 @@ theory CuboidType =
   cuboidCons : Rectangle ⟶ point ⟶ Cuboid ❘ # CuboidCons 1 2 ❙
 ❚
 
+theory PyramidType =
+  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+  include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
+  include ?FrameITBasics ❙
+
+  pyramidType : type ❘ # Pyramid ❙
+  pyramidCons : Rectangle ⟶ point ⟶ Pyramid ❘ # PyramidCons 1 2 ❙
+❚
+
 theory CylinderType =
   include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
   include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
@@ -396,6 +405,7 @@ theory FrameITTheories =
   include ?SphereType ❙
   include ?RectangleType ❙
   include ?CuboidType ❙
+  include ?PyramidType ❙
   include ?CylinderType ❙
 
   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 ❙
diff --git a/source/Scrolls/PyramidScroll.mmt b/source/Scrolls/PyramidScroll.mmt
new file mode 100644
index 0000000..f012b3a
--- /dev/null
+++ b/source/Scrolls/PyramidScroll.mmt
@@ -0,0 +1,31 @@
+namespace http://mathhub.info/FrameIT/frameworld ❚
+fixmeta ?FrameworldMeta ❚
+
+theory PyramidScroll =
+    meta ?MetaAnnotations?problemTheory  ?PyramidScroll/Problem ❙
+    meta ?MetaAnnotations?solutionTheory ?PyramidScroll/Solution ❙
+
+    theory Problem =
+        T: Rectangle
+            ❘ meta ?MetaAnnotations?label "T"
+            ❘ meta ?MetaAnnotations?description "Rectangle"
+        ❙
+        D: point
+            ❘ meta ?MetaAnnotations?label "D"
+            ❘ meta ?MetaAnnotations?description "Point D"
+        ❙
+    ❚
+
+    theory Solution =
+        include ?PyramidScroll/Problem ❙
+
+        meta ?MetaAnnotations?label "Pyramid" ❙
+        meta ?MetaAnnotations?description "Scrolls that takes a rectangle and a points and constructs a Pyramid." ❙
+
+        ConstructedPyramid : pyramidType
+                ❘ = (pyramidCons T D)
+                ❘ meta ?MetaAnnotations?label "Pyramid"
+                ❘ meta ?MetaAnnotations?description "The constructed Pyramid."
+        ❙
+    ❚
+❚
\ No newline at end of file
-- 
GitLab