From 553afe92f2c85ff4fa46aa6d00ff533a592332e2 Mon Sep 17 00:00:00 2001
From: ComFreek <comfreek@outlook.com>
Date: Mon, 26 Oct 2020 17:43:06 +0100
Subject: [PATCH] docs

---
 .../FrameIT/frameworld/$Midpoint.omdoc.xz     | Bin 0 -> 1636 bytes
 errors/mmt-omdoc/Scrolls/MiscScrolls.mmt.err  |   0
 narration/Scrolls/MiscScrolls.omdoc           |   2 +
 relational/Scrolls/MiscScrolls.rel            |   2 +
 .../FrameIT/frameworld/$Midpoint.rel          |  31 +++++++++++++++
 source/Scrolls/MiscScrolls.mmt                |  36 ++++++++++++++++++
 source/Scrolls/README.md                      |  10 +++--
 source/Scrolls/SupplementaryAngles.mmt        |   1 -
 source/Scrolls/TriangleScrolls.mmt            |   3 +-
 9 files changed, 80 insertions(+), 5 deletions(-)
 create mode 100644 content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz
 create mode 100644 errors/mmt-omdoc/Scrolls/MiscScrolls.mmt.err
 create mode 100644 narration/Scrolls/MiscScrolls.omdoc
 create mode 100644 relational/Scrolls/MiscScrolls.rel
 create mode 100644 relational/http..mathhub.info/FrameIT/frameworld/$Midpoint.rel
 create mode 100644 source/Scrolls/MiscScrolls.mmt

diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz
new file mode 100644
index 0000000000000000000000000000000000000000..b819dc1f4052c44f6dedd852b5ba128e5185bc8d
GIT binary patch
literal 1636
zcmV-q2Alc)H+ooF000E$*0e?f03iVu0001VFXf})WJv}hT>u^%$);Gjm;(V8!D4R=
zvOFp-REWkEE1f>j;I%&DeXXhUOC=fH*0Ejij1i?$h>zE3%J*;?T3^ss2<$DwDDq;t
znLacvhp7gSoU4%r5tC(1E<+x$t`yX4RnXQotAgSfL{!=M2;759mLQyA=n&$*h^LUL
zU&mU_$}M;aVe~_8KsQ3DSc6O!aFy&NY{S8wu|@L0!d#%2cCP{3hEkP@K=NnxcXl1X
z(!RUGLDwtJeYC*(>9oF8Nh+~H)TjeVI?M_2FAwbZ_8-%IHm-{y&j0*rLU)?(R^TN?
z>y-A9gWRW2%oUIX<^R&Jr^Js*ynU$PT{1ZZKoI~lLfHz&e{}(rWH})5$kB@F5}ggG
zKcJyM6W$fH5Bo0ciQ&@oAL_H0T^n)<^(I%Y`NX!a9ElyzT^nBJ1RMh2H^@vj4B0IJ
zFav^y<Vl?S>wZw4-Bp0Tf=EE9_Gw=Z;6Hz^GHY@c@L`1V_G?SMt1V9uvEZ~tq!*b}
z^<_Mza(p!BX5l<9EOSu{FKi0OUH6s_fTed#G{Ln%=}?gPM;c^Cty)=GU~#FPesYw2
zqyU!&ihTj6!6k;c^Rxg{;1!b$NTaLgKMJ3cLaE3W>`x4lEmNYIK=@(6W^^PQMNwcC
zYF~o?->~p`6o_)n9W*8IQ-=x87ISP&O=HT_4!O{=d*n4X9L7?};%#f5?Doxl5tBa_
zU3nS^ejS4FG3fiuZ5ANXI6C(A1slFg?4ZjW$*RZWy-~7w@ovGKsEv$91odh7)5w<?
zj%+dxaj!uVr#I7oL+yMXAxW`l@FBsk9^;3D-?ay(*x>(e^B(j7{Sd#AgEsFjjC}Qz
zHri6#bL~U5us`_ds=OY27^+HR9DRS29p`bOP0B#j2*`4z&N7ZH5<#TTd)g9f+n%jZ
zVj5b}p-0TY(ZV*BcQWn}5Uz7#DQm}${hJ*nylc2$S}*#af*Cd}3w;$<&DrjNxOG?e
zP;1VUI<l|dz(tV;{FspApMJwQRgLkIKoa>5WSWq7nx&EAvL%>~cn5|=`+g4PIT}5<
zMi<LV0qpX$$xttY$LPh@LYv9ELBtm5=%>Nf$2lmyUC2E4mOl%{aG*6=00mQxxd9E8
zW;f#Om!ZUo$nF8^jD2!n$nmBpubx)fA46ckWn3D_7z5%Z2f?EXfj;>`!~b0xmJ_df
zd-XlX9!kBBBxRKS;lul+X$>`7#o4alu~c<fU@2Ukk-4zh)Ag$U$(vTpd%~fmL!zDi
z8TLOIe}*a%A)iq<B3qVj3;CrId~eL$(&TL8SF1^ZpunImzXYv1ae@Vy=jw)yJ<#zi
z-J?|PDsZw<cm+wV?un-lFaW(y+PeK1cCV-si;b>g**YcoZpgR_x3;Z=47)ddE7mk_
zn0apw2^1$ke$e=gJW4nvg0DBmpX(6xA{6Yp$IMQufVt$PiA9{-!iOc<c!B=r(O0H`
z6(L22KO1~r5qwg&z60@1_8T2U^k{;89-BnjljMKrSHYzo2U8FTR16F=hm#@ORE78s
ztiha(el(z-fFqsBwMB+e8g=siC3<z!X7GLIh`D4XJR!I^_*#v)rBTw6jkZH(@XEOQ
zb%5IEHKb*CkD&r88=qPx^WTZlxXk>*ne(Ma%wG)Rx7I2wbDH;;^Te^4Lp);Q-FX_S
zLwMAi&~^i{&!gwc4KtUN#Q!w4lvgWLA>kuuF5GfE)|E6ldUQD1rJmVg*K5f)meg04
zU`woQEv78acD`ush*!VKkW>TlK}M5GhXw{)R2^Z3u@WfNqn^FH4v=B5r1^t+S#~Wt
zhC`;srk$3JAZyBb2ln(H;s%`d0_9b^9z}I|ZZ6YU7Ur_GRk}WwBpdC=;<2k+d0DTE
z*Hzb&)Kq$yWe=HB|CtekNTEd4338agDs1a*;gnI2H7~k1=*t!&D@5<t0?J;@B;ykv
zW0X-MZ&pdDiUF4QB@qF6%KAU3aIM(-oOtL+%&_PN1D%4ZJOdaSrJE^di;2K_<QtbD
z3`Q$CZ|4IR#m{H|=WnwEuW_@x@(+tWMQ^lgK}a=MKRK{bFE&WnG`a{uBW_{A0001m
iNx{?xLyWTk0lo~%$N>NXvog7{#Ao{g000001X)^0i6is?

literal 0
HcmV?d00001

diff --git a/errors/mmt-omdoc/Scrolls/MiscScrolls.mmt.err b/errors/mmt-omdoc/Scrolls/MiscScrolls.mmt.err
new file mode 100644
index 0000000..e69de29
diff --git a/narration/Scrolls/MiscScrolls.omdoc b/narration/Scrolls/MiscScrolls.omdoc
new file mode 100644
index 0000000..f8285fa
--- /dev/null
+++ b/narration/Scrolls/MiscScrolls.omdoc
@@ -0,0 +1,2 @@
+<?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
diff --git a/relational/Scrolls/MiscScrolls.rel b/relational/Scrolls/MiscScrolls.rel
new file mode 100644
index 0000000..6c70cd1
--- /dev/null
+++ b/relational/Scrolls/MiscScrolls.rel
@@ -0,0 +1,2 @@
+document http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.omdoc
+Declares http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.omdoc http://mathhub.info/FrameIT/frameworld?Midpoint
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Midpoint.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Midpoint.rel
new file mode 100644
index 0000000..2f362d9
--- /dev/null
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Midpoint.rel
@@ -0,0 +1,31 @@
+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
diff --git a/source/Scrolls/MiscScrolls.mmt b/source/Scrolls/MiscScrolls.mmt
new file mode 100644
index 0000000..412444a
--- /dev/null
+++ b/source/Scrolls/MiscScrolls.mmt
@@ -0,0 +1,36 @@
+/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
diff --git a/source/Scrolls/README.md b/source/Scrolls/README.md
index f0d55f5..90be86b 100644
--- a/source/Scrolls/README.md
+++ b/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
diff --git a/source/Scrolls/SupplementaryAngles.mmt b/source/Scrolls/SupplementaryAngles.mmt
index 1f71182..e643585 100644
--- a/source/Scrolls/SupplementaryAngles.mmt
+++ b/source/Scrolls/SupplementaryAngles.mmt
@@ -1,5 +1,4 @@
 namespace http://mathhub.info/FrameIT/frameworld ❚
-
 fixmeta ?FrameworldMeta ❚
 
 /T
diff --git a/source/Scrolls/TriangleScrolls.mmt b/source/Scrolls/TriangleScrolls.mmt
index 2ba6761..7476814 100644
--- a/source/Scrolls/TriangleScrolls.mmt
+++ b/source/Scrolls/TriangleScrolls.mmt
@@ -1,5 +1,6 @@
-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
-- 
GitLab