docs

narration/Scrolls/MiscScrolls.omdoc

+<?xml version="1.0" encoding="UTF-8"?>
+<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.mmt#0.0.0:1595.42.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.mmt#0.0.0:84.0.84"/></metadata>Miscellaneous scrolls for playing around/testing that don't have a good home yet</opaque><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld?Midpoint]" target="http://mathhub.info/FrameIT/frameworld?Midpoint"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.mmt#165.5.0:179.5.14"/></metadata></mref></omdoc>
\ No newline at end of file

relational/Scrolls/MiscScrolls.rel

+document http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.omdoc
+Declares http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.omdoc http://mathhub.info/FrameIT/frameworld?Midpoint

relational/http..mathhub.info/FrameIT/frameworld/$Midpoint.rel

+theory http://mathhub.info/FrameIT/frameworld?Midpoint
+HasMeta http://mathhub.info/FrameIT/frameworld?Midpoint http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Declares http://mathhub.info/FrameIT/frameworld?Midpoint http://mathhub.info/FrameIT/frameworld?Midpoint?Problem
+theory http://mathhub.info/FrameIT/frameworld?Midpoint/Problem
+HasMeta http://mathhub.info/FrameIT/frameworld?Midpoint/Problem http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Declares http://mathhub.info/FrameIT/frameworld?Midpoint/Problem http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?P
+constant http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?P
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?P?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?P?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+Declares http://mathhub.info/FrameIT/frameworld?Midpoint/Problem http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?Q
+constant http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?Q
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?Q?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?Q?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+Declares http://mathhub.info/FrameIT/frameworld?Midpoint http://mathhub.info/FrameIT/frameworld?Midpoint?Solution
+theory http://mathhub.info/FrameIT/frameworld?Midpoint/Solution
+HasMeta http://mathhub.info/FrameIT/frameworld?Midpoint/Solution http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld?Midpoint/Solution http://mathhub.info/FrameIT/frameworld?Midpoint/Problem
+Declares http://mathhub.info/FrameIT/frameworld?Midpoint/Solution http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint
+constant http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?addition?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?Q?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?P?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition

source/Scrolls/MiscScrolls.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 Midpoint =
+    theory Problem =
+        P
+            : point ❘
+            meta ?MetaAnnotations?label "P" ❘
+            meta ?MetaAnnotations?description "Some arbitrary input point"
+        ❙
+
+        Q
+            : point ❘
+            meta ?MetaAnnotations?label "Q" ❘
+            meta ?MetaAnnotations?description "Some other arbitrary input point"
+        ❙
+    ❚
+
+    theory Solution =
+        include ?Midpoint/Problem ❙
+
+        meta ?MetaAnnotations?label "MidPoint" ❙
+        meta ?MetaAnnotations?problemTheory ?Midpoint/Problem ❙
+        meta ?MetaAnnotations?solutionTheory ?Midpoint/Solution ❙
+        meta ?MetaAnnotations?description s"Our MidPoint scroll that given two points ${lverb P} and ${lverb Q} computes the midpoint of the line ${lverb P Q}." ❙
+
+        midpoint
+            : point ❘
+            = ⟨0.5 ⋅ (P _x + Q _x), 0.5 ⋅ (P _y + Q _y), 0.5 ⋅ (P _z + Q _z)⟩ ❘
+            meta ?MetaAnnotations?label s"Mid[${lverb P Q}]" ❘
+            meta ?MetaAnnotations?description s"The midpoint between points ${lverb P} and ${lverb Q}."
+        ❙
+    ❚
+❚
\ No newline at end of file

source/Scrolls/README.md

@@ -2,7 +2,10 @@
 
 ## How to write one
 
-Let's walk through an example of writing a scroll. For simplicity, let us write a scroll "Midpoint" that requires two points `P` and `Q` as input, and that gives you upon application the midpoint between those points.
+Let's walk through an example of writing a scroll.
+The scroll we will be writing can be found in `MiscScrolls.mmt` at time of writing, albeit without the documentary comments we will be making here.
+
+Let us write a scroll "Midpoint" that requires two points `P` and `Q` as input, and that gives you upon application the midpoint between those points.
 
 ```mmt
 theory Midpoint =
@@ -31,8 +34,8 @@ theory Midpoint =
         include ?Midpoint/Problem ❙
 
         meta ?MetaAnnotations?label "MidPoint" ❙
-        meta ?MetaAnnotations?problemTheory ?AngleSum/Problem ❙
-        meta ?MetaAnnotations?solutionTheory ?AngleSum/Solution ❙
+        meta ?MetaAnnotations?problemTheory ?Midpoint/Problem ❙
+        meta ?MetaAnnotations?solutionTheory ?Midpoint/Solution ❙
 
 
        // In the next meta datum string we prefix the double quotes by an "s"
@@ -54,4 +57,5 @@ theory Midpoint =
             meta ?MetaAnnotations?description s"The midpoint between points ${lverb P} and ${lverb Q}."
         ❙
     ❚
+❚
 ```
\ No newline at end of file

source/Scrolls/SupplementaryAngles.mmt

 namespace http://mathhub.info/FrameIT/frameworld ❚
-
 fixmeta ?FrameworldMeta ❚
 
 /T

source/Scrolls/TriangleScrolls.mmt

-namespace http://mathhub.info/FrameIT/frameworld ❚
+/T Modular scrolls having to do with triangles ❚
 
+namespace http://mathhub.info/FrameIT/frameworld ❚
 fixmeta ?FrameworldMeta ❚
 
 /T A blueprint problem theory for triangle scrolls