Pyramid added

source/DefaultSituationSpace.mmt

@@ -29,6 +29,7 @@ theory DefaultSituationSpace =
         include ?CuboidScroll ❙
         include ?TriangleScroll ❙
         include ?PrismScroll ❙
+        include ?PyramidScroll ❙
         include ?SimpleCircleScroll ❙
         include ?SphereScroll ❙
         include ?CylinderScroll ❙

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 ❙

source/Scrolls/PyramidScroll.mmt

+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