diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz index 8c0bb2a711a6a9f23e9f1848a24ec695edce7d65..9bf20e98a2684f3400455404a40bbf6394732cb6 100644 Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz differ diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz index eac5cab4a80292619b1a927cede9fcd886f5259e..1689fbf227a6048e638804e232045169018ebaf9 100644 Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz differ diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$General$Problem.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$General$Problem.omdoc.xz index 5511dae393b2b5d1a5bf2f7b19a975942bb325a5..a37495953c1feaa9a6e6144f6678ca59acb49fb0 100644 Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$General$Problem.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$General$Problem.omdoc.xz differ diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$Right$Angled$Problem.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$Right$Angled$Problem.omdoc.xz index 9cb883cfbebb09913ded77093cb43307a1c28401..e4f13b5c731a112c3f2db1d8247dc3c22eb8b4b2 100644 Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$Right$Angled$Problem.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$Right$Angled$Problem.omdoc.xz differ diff --git a/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err b/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err index a003a310ddaac2945e140ceaaaa6d7e3db90d6b4..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644 --- a/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err +++ b/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err @@ -1,2 +0,0 @@ -<errors> -</errors> diff --git a/source/Scrolls/README.md b/source/Scrolls/README.md new file mode 100644 index 0000000000000000000000000000000000000000..f0d55f536e441e6493a20cd507f5506401b62c4f --- /dev/null +++ b/source/Scrolls/README.md @@ -0,0 +1,57 @@ +# UFrameIT Scrolls + +## 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. + +```mmt +theory Midpoint = + theory Problem = + // Declare all required fact inputs here. + + For every fact, you may (but are not required to) give some meta information + like a label and description â™ + + 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 = + // note: include the problem theory before spelling out the meta annotations + to have access to the facts formalized in the problem theory â™ + include ?Midpoint/Problem â™ + + meta ?MetaAnnotations?label "MidPoint" â™ + meta ?MetaAnnotations?problemTheory ?AngleSum/Problem â™ + meta ?MetaAnnotations?solutionTheory ?AngleSum/Solution â™ + + + // In the next meta datum string we prefix the double quotes by an "s" + to be able to make use of string interpolation. Concretely, this makes + the scroll dynamic: if the user fills the first P fact slot by a point + with label A, then the scroll description should also talk about A, not P. + + Hence, we use "${lverb P}", where by P we refer to the fact constant of P + as included by the problem theory. Read this as "label verbalization of P". + + And "${lverb P Q}" is syntactic sugar for "${lverb P}${lverb Q}", i.e., the mere + concatenation (without whitespace). â™ + 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_x + Q_x), 0.5 â‹… (P_x + Q_x)⟩ ☠+ 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/TriangleScrolls.mmt b/source/Scrolls/TriangleScrolls.mmt index b45c20aa346ee25868b0628c453636a21a6af0b0..2ba6761cc94f400366a5c69be296afb247d96b50 100644 --- a/source/Scrolls/TriangleScrolls.mmt +++ b/source/Scrolls/TriangleScrolls.mmt @@ -48,13 +48,13 @@ theory AngleSum = âš theory Solution = + include ?AngleSum/Problem â™ + meta ?MetaAnnotations?label "AngleSum" â™ meta ?MetaAnnotations?problemTheory ?AngleSum/Problem â™ meta ?MetaAnnotations?solutionTheory ?AngleSum/Solution â™ meta ?MetaAnnotations?description s"Given a triangle ${lverb A B C} and two known angles, we can deduce the missing angle by the sum of interior angles in triangles always being 180°" â™ - include ?AngleSum/Problem â™ - angleBCA : Σ γ: â„. ⊦ ( ∠B,C,A ) ≠γ ☠= ⟨180.0 - (Ï€l angleBAC) - (Ï€l angleABC), sketch "By sum of interior angles = 180° in triangles"⟩ ☠@@ -115,13 +115,13 @@ theory OppositeLen = âš // theory Solution = + include ?Pythagoras/Problem â™ + meta ?MetaAnnotations?label "Pythagoras" â™ meta ?MetaAnnotations?problemTheory ?Pythagoras/Problem â™ meta ?MetaAnnotations?solutionTheory ?Pythagoras/Solution â™ meta ?MetaAnnotations?description "Given a ABC right-angled at C and lengths of both legs, we can compute the length of the hypotenuse via Pythagora's theorem" â™ - include ?Pythagoras/Problem â™ - deducedHypotenuse : Σ x:â„. ⊦ (d- A B) ≠x ☠= ⟨√ ((Ï€l distanceAC) â‹… (Ï€l distanceAC) + (Ï€l distanceBC) â‹… (Ï€l distanceBC)),