Prism added

source/DefaultSituationSpace.mmt

@@ -28,6 +28,7 @@ theory DefaultSituationSpace =
         include ?RectangleScroll ❙
         include ?CuboidScroll ❙
         include ?TriangleScroll ❙
+        include ?PrismScroll ❙
         include ?SimpleCircleScroll ❙
         include ?SphereScroll ❙
     ❚

source/MetaTheories.mmt

@@ -318,6 +318,15 @@ theory FrameITCylinder =
 
  ❚
 
+theory PrismType =
+  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+  include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
+  include ?FrameITBasics ❙
+
+  prismType : type ❘ # Prism ❙
+  prismCons : triangle ⟶ point ⟶ Prism ❘ # PrismCons 1 2 ❙
+❚
+
 theory CircleType =
   include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
   include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
@@ -372,6 +381,7 @@ theory FrameITTheories =
   include ?FrameITCircle ❙
   include ?FrameITCone ❙
   include ?FrameITCylinder ❙
+  include ?PrismType ❙
   include ?CircleType ❙
   include ?SphereType ❙
   include ?RectangleType ❙

source/Scrolls/PrismScroll.mmt

+namespace http://mathhub.info/FrameIT/frameworld ❚
+fixmeta ?FrameworldMeta ❚
+
+theory PrismScroll =
+    meta ?MetaAnnotations?problemTheory  ?PrismScroll/Problem ❙
+    meta ?MetaAnnotations?solutionTheory ?PrismScroll/Solution ❙
+
+    theory Problem =
+        T: triangle
+            ❘ meta ?MetaAnnotations?label "T"
+            ❘ meta ?MetaAnnotations?description "Triangle"
+        ❙
+        D: point
+            ❘ meta ?MetaAnnotations?label "D"
+            ❘ meta ?MetaAnnotations?description "Point D"
+        ❙
+        dAB: Σ x:ℝ . ⊦ (d- (triangle_point1 T) D) ≐ x
+         ❘ meta ?MetaAnnotations?label s"d${lverb (triangle_point1 T) D}"
+         ❘ meta ?MetaAnnotations?description s"The distance from point ${lverb (triangle_point1 T)} to point ${lverb D}"
+        ❙
+        rDAB: ⊦ (angle_between D (triangle_point1 T) (triangle_point2 T)) ≐ 90.0
+         ❘ meta ?MetaAnnotations?label s"r${lverb D}"
+         ❘ meta ?MetaAnnotations?description s"A right angle between ${lverb D,(triangle_point1 T),(triangle_point2 T)}, where ${lverb D} is the point enclosed by ${lverb (triangle_point1 T)} and ${lverb (triangle_point1 T)}"
+        ❙
+        rDAC: ⊦ (angle_between D (triangle_point1 T) (triangle_point3 T)) ≐ 90.0
+         ❘ meta ?MetaAnnotations?label s"r${lverb D}"
+         ❘ meta ?MetaAnnotations?description s"A right angle between ${lverb D,(triangle_point1 T),(triangle_point3 T)}, where ${lverb D} is the point enclosed by ${lverb (triangle_point1 T)} and ${lverb (triangle_point3 T)}"
+        ❙
+    ❚
+
+    theory Solution =
+        include ?PrismScroll/Problem ❙
+
+        meta ?MetaAnnotations?label "Prism" ❙
+        meta ?MetaAnnotations?description "Scrolls that takes three points and constructs a Prism." ❙
+
+        ConstructedPrism : Prism
+                ❘ = (PrismCons T D)
+                ❘ meta ?MetaAnnotations?label "Prism"
+                ❘ meta ?MetaAnnotations?description "The constructed Prism."
+        ❙
+    ❚
+❚
\ No newline at end of file