From 278c426a67fd95c2891bd913e2b9806b142d9f13 Mon Sep 17 00:00:00 2001
From: Marius Kern <mariusskern@gmail.com>
Date: Sat, 15 Jun 2024 20:49:07 +0200
Subject: [PATCH] Triangle has been worked on

---
 source/MetaTheories.mmt           |  1 -
 source/Scrolls/TriangleScroll.mmt | 18 +++++++++---------
 source/Scrolls/TriangleType.mmt   | 18 ------------------
 3 files changed, 9 insertions(+), 28 deletions(-)
 delete mode 100644 source/Scrolls/TriangleType.mmt

diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt
index 23a77a7..6bc7cb5 100644
--- a/source/MetaTheories.mmt
+++ b/source/MetaTheories.mmt
@@ -337,7 +337,6 @@ theory FrameworldMeta =
   include ?FrameITTheories ❙
   include ?RectangleType ❙
   include ?CuboidType ❙
-  include ?TriangleType ❙
   include ?CircleType ❙
 
  // include ☞http://mathhub.info/MitM/core/arithmetics?RealArithmetics ❙
diff --git a/source/Scrolls/TriangleScroll.mmt b/source/Scrolls/TriangleScroll.mmt
index 0461a28..78d0e6a 100644
--- a/source/Scrolls/TriangleScroll.mmt
+++ b/source/Scrolls/TriangleScroll.mmt
@@ -18,19 +18,19 @@ theory TriangleScroll =
             ❘ meta ?MetaAnnotations?label "C"
             ❘ meta ?MetaAnnotations?description "The third point"
         ❙
-        // D: point
+        D: point
             ❘ meta ?MetaAnnotations?label "D"
             ❘ meta ?MetaAnnotations?description "The fourth point"
         ❙
-        // dAB: Σ x:ℝ . ⊦ (d- A B) ≐ x
+        dAB: Σ x:ℝ . ⊦ (d- A B) ≐ x
          ❘ meta ?MetaAnnotations?label s"d${lverb A B}"
          ❘ meta ?MetaAnnotations?description s"The distance from point ${lverb A} to point ${lverb B}"
         ❙
-        // dDC: Σ x:ℝ . ⊦ (d- D C) ≐ x
+        dDC: Σ x:ℝ . ⊦ (d- D C) ≐ x
          ❘ meta ?MetaAnnotations?label s"d${lverb D C}"
          ❘ meta ?MetaAnnotations?description s"The distance from point ${lverb D} to point ${lverb C}"
         ❙
-        // rADC: ⊦ (∠ A,D,C) ≐ 90.0
+        rADC: ⊦ (∠ A,D,C) ≐ 90.0
          ❘ meta ?MetaAnnotations?label s"r${lverb D}"
          ❘ meta ?MetaAnnotations?description s"A right angle between ${lverb A D C}, where ${lverb D} is the point enclosed by ${lverb A} and ${lverb C}"
         ❙
@@ -40,12 +40,12 @@ theory TriangleScroll =
         include ?TriangleScroll/Problem ❙
 
         meta ?MetaAnnotations?label "Triangle" ❙
-        meta ?MetaAnnotations?description s"Scrolls that takes three points and constructs a triangle." ❙
+        meta ?MetaAnnotations?description "Scrolls that takes three points and constructs a triangle." ❙
 
-        ConstructedTriangle : Triangle
-                ❘ = TriangleCons A B C
-                ❘ meta ?MetaAnnotations?label s"Triangle"
-                ❘ meta ?MetaAnnotations?description s"The constructed Triangle."
+        ConstructedTriangle : triangle
+                ❘ = (triangle_constructor A B C)
+                ❘ meta ?MetaAnnotations?label "Triangle"
+                ❘ meta ?MetaAnnotations?description "The constructed Triangle."
         ❙
     ❚
 ❚
\ No newline at end of file
diff --git a/source/Scrolls/TriangleType.mmt b/source/Scrolls/TriangleType.mmt
deleted file mode 100644
index 4fd656b..0000000
--- a/source/Scrolls/TriangleType.mmt
+++ /dev/null
@@ -1,18 +0,0 @@
-namespace http://mathhub.info/FrameIT/frameworld ❚
-fixmeta ur:?LF ❚
-
-theory TriangleType =
-    include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
-    include ?FrameITBasics ❙
-
-    triangleType : type ❘ # Triangle ❙
-    triangleCons : point ⟶ point ⟶ point ⟶ Triangle ❘ # TriangleCons 1 2 3 ❙
-
-    // triangleA : triangle ⟶ point ❘ # triangleA 1 ❙
-    // triangleB : triangle ⟶ point ❘ # triangleB 1 ❙
-    // triangleC : triangle ⟶ point ❘ # triangleC 1 ❙
-
-    // axTriangleA : {a, b, c} ⊦ triangleA (triangleCons a b c) ≐ a  ❘ role Simplify ❙
-    // axTriangleB : {a, b, c} ⊦ triangleB (triangleCons a b c) ≐ b  ❘ role Simplify ❙
-    // axTriangleC : {a, b, c} ⊦ triangleC (triangleCons a b c) ≐ c  ❘ role Simplify ❙
-❚
\ No newline at end of file
-- 
GitLab