From 1a4227b976957aa81dc71f16efd0f88d16398d0f Mon Sep 17 00:00:00 2001
From: Paul-Walcher <paulwalcher12@gmail.com>
Date: Sat, 29 Jun 2024 08:58:58 +0200
Subject: [PATCH] cylinder Type added

---
 source/MetaTheories.mmt | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt
index 038f01f..6a830cc 100644
--- a/source/MetaTheories.mmt
+++ b/source/MetaTheories.mmt
@@ -373,6 +373,16 @@ theory CuboidType =
   cuboidCons : Rectangle ⟶ point ⟶ Cuboid ❘ # CuboidCons 1 2 ❙
 ❚
 
+theory CylinderType =
+  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+  include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
+  include ?FrameITBasics ❙
+  include ?FrameITCircle ❙
+
+  cylinderType : type ❘ # Cylinder ❙
+  cylinderCons : circle ⟶ point ⟶ Cylinder ❘ # CylinderCons 1 2 ❙
+❚
+
 theory FrameITTheories =
   include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
   include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
-- 
GitLab