From 29f324020313edfad8507a256188177bba0b6486 Mon Sep 17 00:00:00 2001
From: Paul-Walcher <paulwalcher12@gmail.com>
Date: Sat, 1 Jun 2024 13:47:53 +0200
Subject: [PATCH] square

---
 DOC/Add_scroll_to_unity.md       |  8 +++---
 source/DefaultSituationSpace.mmt |  4 ++-
 source/MetaTheories.mmt          |  2 ++
 source/Scrolls/Square.mmt        | 15 -----------
 source/Scrolls/SquareScroll.mmt  | 45 ++++++++++++++++++--------------
 source/Scrolls/SquareType.mmt    | 12 +++++++++
 6 files changed, 48 insertions(+), 38 deletions(-)
 delete mode 100644 source/Scrolls/Square.mmt
 create mode 100644 source/Scrolls/SquareType.mmt

diff --git a/DOC/Add_scroll_to_unity.md b/DOC/Add_scroll_to_unity.md
index 7a31ae2..39e6c83 100644
--- a/DOC/Add_scroll_to_unity.md
+++ b/DOC/Add_scroll_to_unity.md
@@ -12,8 +12,10 @@ In archives:
 In uframeit 
 1. add your scroll to "UFrameIT\Assets\Scripts\MMTServer\CommunicationProtocoll\MMTConstants.cs"\
 
-if Class "GlobalBehaviour" ("UFrameIT\Assets\Scripts\GlobalBehaviour.cs") Method "GetScrollsfromServer()" loads scrolls from "UFrameIT\Assets\StreamingAssets\scrolls.json":
+2. Add the MMT-constructor you Implemented into Assets\Scripts\MMTServer\CommunicationProtocol\MMTConstants.cs
 
-2. Open: "http://localhost:8085/scroll/list" and copy all the text.
+in Class "GlobalBehaviour" ("UFrameIT\Assets\Scripts\GlobalBehaviour.cs") Method "GetScrollsfromServer()" loads scrolls from "UFrameIT\Assets\StreamingAssets\scrolls.json":
 
-3. Now paste this into: "UFrameIT\Assets\StreamingAssets\scrolls.json" and start the game.
\ No newline at end of file
+3. Open: "http://localhost:8085/scroll/list" and copy all the text.
+
+4. Now paste this into: "UFrameIT\Assets\StreamingAssets\scrolls.json" and start the game.
\ No newline at end of file
diff --git a/source/DefaultSituationSpace.mmt b/source/DefaultSituationSpace.mmt
index 77d0596..40f028c 100644
--- a/source/DefaultSituationSpace.mmt
+++ b/source/DefaultSituationSpace.mmt
@@ -16,18 +16,20 @@ theory DefaultSituationSpace =
         include ?Midpoint ❙
         include ?Test ❙
         include ?CircleScroll ❙
+        
         include ?MuchBetterCircleScroll ❙
 		include ?BouncingScroll ❙
         include ?WBouncingScroll ❙
         include ?W3DBouncingScroll ❙
         include ?T3DBouncingScroll ❙
       //  include ?SinOppositeLeg ❙
-        include ?Square ❙
         include ?CircleLineAngleScroll ❙
         include ?CircleAreaScroll ❙
         include ?ConeVolumeScroll ❙
         include ?TruncatedConeVolumeScroll ❙
         include ?SquareScroll ❙
+        
+
 
 
     ❚
diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt
index 644d6a7..f46f039 100644
--- a/source/MetaTheories.mmt
+++ b/source/MetaTheories.mmt
@@ -3,6 +3,7 @@ namespace http://mathhub.info/FrameIT/frameworld ❚
 
 fixmeta ur:?LF ❚
 
+
 /T MMT meta keys and value constructors for meta annotations of facts in situation theories and (input/output) facts in scrolls ❚
 theory MetaAnnotations =
     include ☞http://mathhub.info/MitM/Foundation?Strings ❙
@@ -334,6 +335,7 @@ theory FrameITTheories =
 theory FrameworldMeta =
   include ?MetaAnnotations ❙
   include ?FrameITTheories ❙
+  include ?SquareType ❙
 
  // include ☞http://mathhub.info/MitM/core/arithmetics?RealArithmetics ❙
 
diff --git a/source/Scrolls/Square.mmt b/source/Scrolls/Square.mmt
deleted file mode 100644
index 3d62c8c..0000000
--- a/source/Scrolls/Square.mmt
+++ /dev/null
@@ -1,15 +0,0 @@
-namespace http://mathhub.info/MitM/core/geometry ❚
-
-import base http://mathhub.info/MitM/Foundation ❚
-import arith http://mathhub.info/MitM/core/arithmetics ❚
-
-fixmeta base:?Logic ❚
-
-theory Square =
-
-    include ☞base:?ProductTypes ❙
-
-    square: type ❘ # square ❙
-    square_cons: point ⟶ point ⟶ point ⟶ point ⟶ square ❘ # square_cons 1 2 3 4 ❙
-
-❚
\ No newline at end of file
diff --git a/source/Scrolls/SquareScroll.mmt b/source/Scrolls/SquareScroll.mmt
index fc3fbf6..57371de 100644
--- a/source/Scrolls/SquareScroll.mmt
+++ b/source/Scrolls/SquareScroll.mmt
@@ -1,38 +1,45 @@
 
 /T Miscellaneous scrolls for playing around/testing that don't have a good home yet  ❚
 
+/T Miscellaneous scrolls for playing around/testing that don't have a good home yet  ❚
 namespace http://mathhub.info/FrameIT/frameworld ❚
 fixmeta ?FrameworldMeta ❚
 
 
-
 theory SquareScroll =
     meta ?MetaAnnotations?problemTheory  ?SquareScroll/Problem ❙
     meta ?MetaAnnotations?solutionTheory ?SquareScroll/Solution ❙
     theory Problem =
+        A: point
+         ❘ meta ?MetaAnnotations?label "A"
+         ❘ meta ?MetaAnnotations?description "The first point"
+        ❙
+        B: point
+         ❘ meta ?MetaAnnotations?label "B"
+         ❘ meta ?MetaAnnotations?description "The second point"
+        ❙
+        C: point
+         ❘ meta ?MetaAnnotations?label "C"
+         ❘ meta ?MetaAnnotations?description "The third point"
+        ❙
+
+        rC: ⊦ (∠ A,B,C) ≐ 90.0
+         ❘ meta ?MetaAnnotations?label "C"
+         ❘ meta ?MetaAnnotations?description "The third point"
+        ❙
 
-        A: point ❘ meta ?MetaAnnotations?label "A" ❙
-        B: point ❘ meta ?MetaAnnotations?label "B"❙
-        C: point ❘ meta ?MetaAnnotations?label "C"❙
 
-        rightAngleC
-        : ⊦∠A,B,C≐90.0 ❘
-        meta ?MetaAnnotations?label s"⊾${lverb C}"  ❘
-        meta ?MetaAnnotations?description s"${lverb A C} ⟂ ${lverb B C}: right angle at ${lverb C} as enclosed by legs ${lverb A C} and ${lverb B C}."
     ❙
-
-
+        
     ❚
     theory Solution =
         include ?SquareScroll/Problem ❙
-        meta ?MetaAnnotations?label "SquareScroll" ❙
-        meta ?MetaAnnotations?description s"Square Scroll Constructing a Square" ❙
-
-        construct_square: square
-                ❘ = square_cons A A A A
-                ❘ meta ?MetaAnnotations?label s"E"
-                ❘ meta ?MetaAnnotations?description s"EE"
-                ❙
-
+        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}." ❙
+        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}."
+        ❙
     ❚
 ❚
\ No newline at end of file
diff --git a/source/Scrolls/SquareType.mmt b/source/Scrolls/SquareType.mmt
new file mode 100644
index 0000000..aa6fb72
--- /dev/null
+++ b/source/Scrolls/SquareType.mmt
@@ -0,0 +1,12 @@
+namespace http://mathhub.info/FrameIT/frameworld ❚
+fixmeta ur:?LF ❚
+
+theory SquareType =
+  
+  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+  include ?FrameITBasics ❙
+
+  squareType : type ❘ # Square ❙
+  squareCons : point ⟶ point ⟶ point  ⟶ Square  ❘ # SquareCons 1 2 3 ❙
+  
+❚
\ No newline at end of file
-- 
GitLab