upload

source/DefaultSituationSpace.mmt

@@ -16,15 +16,18 @@ 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/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  ❚
+
+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" ❙
+        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"
+                ❙
+
+    ❚
+❚
\ No newline at end of file