From f3e5e1ee36b67a922c5a8d080e6421f4ca5ec0d7 Mon Sep 17 00:00:00 2001
From: Marius Kern <mariusskern@gmail.com>
Date: Fri, 2 Aug 2024 15:47:54 +0200
Subject: [PATCH] Pyramid

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

diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt
index 98311f4..b4a0122 100644
--- a/source/MetaTheories.mmt
+++ b/source/MetaTheories.mmt
@@ -377,6 +377,7 @@ theory PyramidType =
   include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
   include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
   include ?FrameITBasics ❙
+  include ?RectangleType ❙
 
   pyramidType : type ❘ # Pyramid ❙
   pyramidCons : Rectangle ⟶ point ⟶ Pyramid ❘ # PyramidCons 1 2 ❙
-- 
GitLab