From e97a2032a93783daa787a2da4cece205bb3250f4 Mon Sep 17 00:00:00 2001
From: Marius Kern <mariusskern@gmail.com>
Date: Thu, 27 Jun 2024 18:21:47 +0200
Subject: [PATCH] Prism

---
 source/Scrolls/PrismScroll.mmt | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/source/Scrolls/PrismScroll.mmt b/source/Scrolls/PrismScroll.mmt
index 90ec599..3090df6 100644
--- a/source/Scrolls/PrismScroll.mmt
+++ b/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."
         ❙
-- 
GitLab