diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt index 23a77a7a928f380052dbbe33e379d0094ccd5a3d..6bc7cb56e419cf772b07df76dbf735ca70f8e631 100644 --- a/source/MetaTheories.mmt +++ b/source/MetaTheories.mmt @@ -337,7 +337,6 @@ theory FrameworldMeta = include ?FrameITTheories ♠include ?RectangleType ♠include ?CuboidType ♠- include ?TriangleType ♠include ?CircleType ♠// include ☞http://mathhub.info/MitM/core/arithmetics?RealArithmetics ♠diff --git a/source/Scrolls/TriangleScroll.mmt b/source/Scrolls/TriangleScroll.mmt index 0461a28489468c1930ad8650a809e5ed98f46672..78d0e6aad2ed4201ed74e32401b49a460ae25ea8 100644 --- a/source/Scrolls/TriangleScroll.mmt +++ b/source/Scrolls/TriangleScroll.mmt @@ -18,19 +18,19 @@ theory TriangleScroll = ☠meta ?MetaAnnotations?label "C" ☠meta ?MetaAnnotations?description "The third point" ♠- // D: point + D: point ☠meta ?MetaAnnotations?label "D" ☠meta ?MetaAnnotations?description "The fourth point" ♠- // dAB: Σ x:℠. ⊦ (d- A B) ≠x + dAB: Σ x:℠. ⊦ (d- A B) ≠x ☠meta ?MetaAnnotations?label s"d${lverb A B}" ☠meta ?MetaAnnotations?description s"The distance from point ${lverb A} to point ${lverb B}" ♠- // dDC: Σ x:℠. ⊦ (d- D C) ≠x + dDC: Σ x:℠. ⊦ (d- D C) ≠x ☠meta ?MetaAnnotations?label s"d${lverb D C}" ☠meta ?MetaAnnotations?description s"The distance from point ${lverb D} to point ${lverb C}" ♠- // rADC: ⊦ (∠A,D,C) ≠90.0 + rADC: ⊦ (∠A,D,C) ≠90.0 ☠meta ?MetaAnnotations?label s"r${lverb D}" ☠meta ?MetaAnnotations?description s"A right angle between ${lverb A D C}, where ${lverb D} is the point enclosed by ${lverb A} and ${lverb C}" ♠@@ -40,12 +40,12 @@ theory TriangleScroll = include ?TriangleScroll/Problem ♠meta ?MetaAnnotations?label "Triangle" ♠- meta ?MetaAnnotations?description s"Scrolls that takes three points and constructs a triangle." ♠+ meta ?MetaAnnotations?description "Scrolls that takes three points and constructs a triangle." ♠- ConstructedTriangle : Triangle - ☠= TriangleCons A B C - ☠meta ?MetaAnnotations?label s"Triangle" - ☠meta ?MetaAnnotations?description s"The constructed Triangle." + ConstructedTriangle : triangle + ☠= (triangle_constructor A B C) + ☠meta ?MetaAnnotations?label "Triangle" + ☠meta ?MetaAnnotations?description "The constructed Triangle." ♠⚠⚠\ No newline at end of file diff --git a/source/Scrolls/TriangleType.mmt b/source/Scrolls/TriangleType.mmt deleted file mode 100644 index 4fd656b01b1e7da41b099dedde8abf6c92e51c9e..0000000000000000000000000000000000000000 --- a/source/Scrolls/TriangleType.mmt +++ /dev/null @@ -1,18 +0,0 @@ -namespace http://mathhub.info/FrameIT/frameworld ⚠-fixmeta ur:?LF ⚠- -theory TriangleType = - include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ♠- include ?FrameITBasics ♠- - triangleType : type ☠# Triangle ♠- triangleCons : point ⟶ point ⟶ point ⟶ Triangle ☠# TriangleCons 1 2 3 ♠- - // triangleA : triangle ⟶ point ☠# triangleA 1 ♠- // triangleB : triangle ⟶ point ☠# triangleB 1 ♠- // triangleC : triangle ⟶ point ☠# triangleC 1 ♠- - // axTriangleA : {a, b, c} ⊦ triangleA (triangleCons a b c) ≠a ☠role Simplify ♠- // axTriangleB : {a, b, c} ⊦ triangleB (triangleCons a b c) ≠b ☠role Simplify ♠- // axTriangleC : {a, b, c} ⊦ triangleC (triangleCons a b c) ≠c ☠role Simplify ♠-⚠\ No newline at end of file