Triangle has been worked on

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 ❙

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

source/Scrolls/TriangleType.mmt

-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