diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt index aedd54df9a87c83b3f8ff6e5307b8430c9efba08..10b4921ac62331f69f283eee8ad913a7d1c1a539 100644 --- a/source/MetaTheories.mmt +++ b/source/MetaTheories.mmt @@ -344,6 +344,14 @@ theory RectangleType = rectangleType : type ☠# Rectangle ♠rectangleCons : point ⟶ point ⟶ point ⟶ Rectangle ☠# RectangleCons 1 2 3 ♠+ + getA : Rectangle ⟶ point ☠# getA 1 ♠+ getB : Rectangle ⟶ point ☠# getB 1 ♠+ getC : Rectangle ⟶ point ☠# getC 1 ♠+ + getAAxiom : {A, B, C} ⊦ ( ( getA ( RectangleCons A B C) ) ≠A ) ☠role Simplify♠+ getBAxiom : {A, B, C} ⊦ ( ( getB ( RectangleCons A B C) ) ≠B ) ☠role Simplify♠+ getCAxiom : {A, B, C} ⊦ ( ( getC ( RectangleCons A B C) ) ≠C ) ☠role Simplify♠⚠theory CuboidType = diff --git a/source/Scrolls/CuboidScroll.mmt b/source/Scrolls/CuboidScroll.mmt index 645630d0c6bcbe7eefcbb15efea4149ebd59ea05..f7e6729dadbaac7d0751bbb167bfdbf6a709ba0c 100644 --- a/source/Scrolls/CuboidScroll.mmt +++ b/source/Scrolls/CuboidScroll.mmt @@ -20,6 +20,16 @@ theory CuboidScroll = ☠meta ?MetaAnnotations?description "The point above the centerpoint of the rectangle" ♠+ rTBA: ⊦ (∠T,(getB R),(getA R)) ≠90.0 + ☠meta ?MetaAnnotations?label "rTBA" + ☠meta ?MetaAnnotations?description "A right angle between TBA, where B is the point enclosed by T A" + ♠+ + rTBC: ⊦ (∠T,(getB R),(getC R)) ≠90.0 + ☠meta ?MetaAnnotations?label "rTBC" + ☠meta ?MetaAnnotations?description "A right angle between TBC, where B is the point enclosed by T C" + ♠+ ⚠theory Solution =