docs

errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err

-<errors>
-</errors>

source/Scrolls/README.md

+# 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

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)),