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 Binary files /dev/null and b/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz differ diff --git a/errors/mmt-omdoc/Scrolls/MiscScrolls.mmt.err b/errors/mmt-omdoc/Scrolls/MiscScrolls.mmt.err new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/narration/Scrolls/MiscScrolls.omdoc b/narration/Scrolls/MiscScrolls.omdoc new file mode 100644 index 0000000000000000000000000000000000000000..f8285fa7c1c45a42332b4d38c3d7a1c256ae22f2 --- /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 0000000000000000000000000000000000000000..6c70cd1e0fb0c180087387b4386989127f8b65ef --- /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 0000000000000000000000000000000000000000..2f362d918602781d8889765303d713655b579deb --- /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 0000000000000000000000000000000000000000..412444a5fea73789f717dadf70a47d23d782e0ac --- /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 f0d55f536e441e6493a20cd507f5506401b62c4f..90be86bed2e044724b516c146e8a0fcba3dc2e78 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 1f711821a298bcc7c4cf14dad5aadfc34c7b71e7..e64358543c69f3feca94940fb7322983e4940e79 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 2ba6761cc94f400366a5c69be296afb247d96b50..74768140fc297724f4258b4b8fd2eb2bd113a1f3 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