square

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.
+3. Open: "http://localhost:8085/scroll/list" and copy all the text.
\ No newline at end of file
+
+4. Now paste this into: "UFrameIT\Assets\StreamingAssets\scrolls.json" and start the game.
\ No newline at end of file

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 ❙
+        
+
 
 
     ❚

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 ❙
 

source/Scrolls/Square.mmt

-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

source/Scrolls/SquareScroll.mmt

 
 /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

source/Scrolls/SquareType.mmt

+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