Prism

source/Scrolls/PrismScroll.mmt

@@ -14,15 +14,15 @@ theory PrismScroll =
             ❘ meta ?MetaAnnotations?label "D"
             ❘ meta ?MetaAnnotations?description "Point D"
         ❙
-        dAB: Σ x:ℝ . ⊦ (d- (triangle_point1 T) D) ≐ x
+        // dAB: Σ x:ℝ . ⊦ (d- (triangle_point1 T) D) ≐ x
          ❘ meta ?MetaAnnotations?label s"d${lverb (triangle_point1 T) D}"
          ❘ meta ?MetaAnnotations?description s"The distance from point ${lverb (triangle_point1 T)} to point ${lverb D}"
         ❙
-        rDAB: ⊦ (angle_between D (triangle_point1 T) (triangle_point2 T)) ≐ 90.0
+        // rDAB: ⊦ (angle_between D (triangle_point1 T) (triangle_point2 T)) ≐ 90.0
          ❘ meta ?MetaAnnotations?label s"r${lverb D}"
          ❘ meta ?MetaAnnotations?description s"A right angle between ${lverb D,(triangle_point1 T),(triangle_point2 T)}, where ${lverb D} is the point enclosed by ${lverb (triangle_point1 T)} and ${lverb (triangle_point1 T)}"
         ❙
-        rDAC: ⊦ (angle_between D (triangle_point1 T) (triangle_point3 T)) ≐ 90.0
+        // rDAC: ⊦ (angle_between D (triangle_point1 T) (triangle_point3 T)) ≐ 90.0
          ❘ meta ?MetaAnnotations?label s"r${lverb D}"
          ❘ meta ?MetaAnnotations?description s"A right angle between ${lverb D,(triangle_point1 T),(triangle_point3 T)}, where ${lverb D} is the point enclosed by ${lverb (triangle_point1 T)} and ${lverb (triangle_point3 T)}"
         ❙
@@ -34,8 +34,8 @@ theory PrismScroll =
         meta ?MetaAnnotations?label "Prism" ❙
         meta ?MetaAnnotations?description "Scrolls that takes three points and constructs a Prism." ❙
 
-        ConstructedPrism : Prism
-                ❘ = (PrismCons T D)
+        ConstructedPrism : prismType
+                ❘ = (prismCons T D)
                 ❘ meta ?MetaAnnotations?label "Prism"
                 ❘ meta ?MetaAnnotations?description "The constructed Prism."
         ❙