diff --git a/source/DefaultSituationSpace.mmt b/source/DefaultSituationSpace.mmt index 29994d4683200734697d089eccb11007ee1a5139..b6b42f4d2a57fb1ac28b65a215ef643ca1294aca 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 c405bff63420774e936d4ee2c2e468d21afcc0c9..98311f40f85043eef2d85c1b8f233da80eb2a3da 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 0000000000000000000000000000000000000000..f012b3a0daffe4efdc80a3f948653f194e3ce708 --- /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