From a4c8def66ecaa62cb06fa7ed634decc25b6f6e73 Mon Sep 17 00:00:00 2001
From: Paul-Walcher <paulwalcher12@gmail.com>
Date: Thu, 4 Jul 2024 17:24:12 +0200
Subject: [PATCH] Updated Cylinder

---
 source/MetaTheories.mmt           | 4 ++--
 source/Scrolls/CylinderScroll.mmt | 6 +-----
 2 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt
index c9dceb2..c405bff 100644
--- a/source/MetaTheories.mmt
+++ b/source/MetaTheories.mmt
@@ -379,8 +379,8 @@ theory CylinderType =
   include ?FrameITBasics ❙
 
   cylinderType : type ❘ # Cylinder ❙
-  // takes a midpoint, a point on the edge of the base-circle plane, as well as a point in the base-circle plane, and a point directly above the midpoint  ❙
-  cylinderCons : point ⟶ point ⟶ point ⟶ point ⟶ Cylinder ❘ # CylinderCons 1 2 3 4 ❙
+  // takes a midpoint, a point on the edge of the base-circle plane and a point directly above the midpoint  ❙
+  cylinderCons : point ⟶ point ⟶ point ⟶ Cylinder ❘ # CylinderCons 1 2 3 ❙
 ❚
 
 theory FrameITTheories =
diff --git a/source/Scrolls/CylinderScroll.mmt b/source/Scrolls/CylinderScroll.mmt
index 20149f5..e78d12a 100644
--- a/source/Scrolls/CylinderScroll.mmt
+++ b/source/Scrolls/CylinderScroll.mmt
@@ -15,10 +15,6 @@ theory CylinderScroll =
          ❘ meta ?MetaAnnotations?label "E"
          ❘ meta ?MetaAnnotations?description "The point on the edge of the bottom-circle-plane"
         ❙
-        P: point
-         ❘ meta ?MetaAnnotations?label "P"
-         ❘ meta ?MetaAnnotations?description "A point in the bottom-circle-plane"
-        ❙
         T: point
          ❘ meta ?MetaAnnotations?label "T"
          ❘ meta ?MetaAnnotations?description "The point directly above the point M"
@@ -32,7 +28,7 @@ theory CylinderScroll =
         meta ?MetaAnnotations?label "Cylinder" ❙
         meta ?MetaAnnotations?description s"Given four points: Three points that form the bottom-plane and one directly above this scroll constructs a cylinder" ❙
         ConstructedCylinder: Cylinder
-                ❘ = ( CylinderCons M E P T )
+                ❘ = ( CylinderCons M E T )
                 ❘ meta ?MetaAnnotations?label s"Cylinder"
                 ❘ meta ?MetaAnnotations?description s"The constructed Cylinder."
         ❙
-- 
GitLab