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

---
 source/Scrolls/TriangleScroll.mmt | 16 ++++++++++++++++
 source/Scrolls/TriangleType.mmt   |  8 ++++++++
 2 files changed, 24 insertions(+)

diff --git a/source/Scrolls/TriangleScroll.mmt b/source/Scrolls/TriangleScroll.mmt
index 913f431..0461a28 100644
--- a/source/Scrolls/TriangleScroll.mmt
+++ b/source/Scrolls/TriangleScroll.mmt
@@ -18,6 +18,22 @@ theory TriangleScroll =
             ❘ meta ?MetaAnnotations?label "C"
             ❘ meta ?MetaAnnotations?description "The third point"
         ❙
+        // D: point
+            ❘ meta ?MetaAnnotations?label "D"
+            ❘ meta ?MetaAnnotations?description "The fourth point"
+        ❙
+        // 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
+         ❘ 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
+         ❘ 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}"
+        ❙
     ❚
 
     theory Solution =
diff --git a/source/Scrolls/TriangleType.mmt b/source/Scrolls/TriangleType.mmt
index da5f198..4fd656b 100644
--- a/source/Scrolls/TriangleType.mmt
+++ b/source/Scrolls/TriangleType.mmt
@@ -7,4 +7,12 @@ theory TriangleType =
 
     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