diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt index c9dceb29975ec1fd9be2cc56f96ac062cab07657..c405bff63420774e936d4ee2c2e468d21afcc0c9 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 20149f58c95f9f3d458463da648955492ce4ebfa..e78d12a4e6bb54e8c09f058bdfc6f3398bea3813 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." â™