From dfd4f338f5f8fe79e4ae4c824a543d1de2428c8b Mon Sep 17 00:00:00 2001
From: Paul-Walcher <paulwalcher12@gmail.com>
Date: Mon, 10 Jun 2024 09:20:55 +0200
Subject: [PATCH] Changed SquareScroll and Circle Scroll

Added additional conditions for construction:

Square: Distance AB and Distance BC, so that inuitively the area is dAB * dBC.

Circle: The distance from thew center to the edgepoint, also for providing a more intuitive way to construct circles.
---
 source/Scrolls/CircleScroll.mmt |  3 +++
 source/Scrolls/SquareScroll.mmt | 21 ++++++++++++++++-----
 2 files changed, 19 insertions(+), 5 deletions(-)

diff --git a/source/Scrolls/CircleScroll.mmt b/source/Scrolls/CircleScroll.mmt
index 811c564..82861a9 100644
--- a/source/Scrolls/CircleScroll.mmt
+++ b/source/Scrolls/CircleScroll.mmt
@@ -16,6 +16,9 @@ theory CircleScroll =
                   ❘ meta ?MetaAnnotations?description "A point on the circle" ❙
         B : point ❘ meta ?MetaAnnotations?label "B"
                   ❘ meta ?MetaAnnotations?description "A point within the plane the circle should lie in." ❙
+        dMA : Σ x:ℝ . ⊦ (d- M A) ≐ x
+                  ❘ meta ?MetaAnnotations?label "dMA"
+                  ❘ meta ?MetaAnnotations?description "The distance from the Midpoint M to the edge point A" ❙
     ❚
 
     theory Solution =
diff --git a/source/Scrolls/SquareScroll.mmt b/source/Scrolls/SquareScroll.mmt
index 57371de..ea84c98 100644
--- a/source/Scrolls/SquareScroll.mmt
+++ b/source/Scrolls/SquareScroll.mmt
@@ -24,8 +24,18 @@ theory SquareScroll =
         ❙
 
         rC: ⊦ (∠ A,B,C) ≐ 90.0
-         ❘ meta ?MetaAnnotations?label "C"
-         ❘ meta ?MetaAnnotations?description "The third point"
+         ❘ meta ?MetaAnnotations?label "rC"
+         ❘ meta ?MetaAnnotations?description "A right angle between ABC, where B is the point enclosed by A and B"
+        ❙
+
+        dAB: Σ x:ℝ . ⊦ (d- A B) ≐ x
+         ❘ meta ?MetaAnnotations?label "dAB"
+         ❘ meta ?MetaAnnotations?description "The distance from point A to point B"
+        ❙
+
+        dBC: Σ x:ℝ . ⊦ (d- B C) ≐ x
+         ❘ meta ?MetaAnnotations?label "dBC"
+         ❘ meta ?MetaAnnotations?description "The distance from point B to point C"
         ❙
 
 
@@ -35,11 +45,12 @@ theory SquareScroll =
     theory Solution =
         include ?SquareScroll/Problem ❙
         meta ?MetaAnnotations?label "Square" ❙
-        meta ?MetaAnnotations?description s"Our Test scroll that given two points ${lverb P} and ${lverb Q} computes the Test of the line ${lverb P Q}." ❙
+        meta ?MetaAnnotations?description s"Scrolls that takes three points and given a right-angle fact between those points
+                                            and the distances from the first to the second and the second to the third point, constructs a rectangle." ❙
         ConstructedSquare : Square
                 ❘ = SquareCons A B C
-                ❘ meta ?MetaAnnotations?label s"Mid[${lverb P Q}]"
-                ❘ meta ?MetaAnnotations?description s"The Test between points ${lverb P} and ${lverb Q}."
+                ❘ meta ?MetaAnnotations?label s"Square"
+                ❘ meta ?MetaAnnotations?description s"The constructed Square."
         ❙
     ❚
 ❚
\ No newline at end of file
-- 
GitLab