diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt index b4a01226e2ad74e2f83aae5953dd2a6fa0c6a5a0..4bf9b90607c31ca81f0e9c58943c777b2782eea0 100644 --- a/source/MetaTheories.mmt +++ b/source/MetaTheories.mmt @@ -121,7 +121,7 @@ theory FrameITRectangles = // TODO maybe delete ♠rectangle_type : type ☠# rect ♠- testPoint_type : type ☠# testPoint ♠+ mkRectangle : { A: point , B : point, C : point , D : point } ( ⊦ isRect A B C D ) ⟶ rect ☠# mkRect 1 2 3 4 5 ♠cornerA : rect ⟶ point ☠# rectA 1 ♠diff --git a/source/Scrolls/Test.mmt b/source/Scrolls/Test.mmt deleted file mode 100644 index 37049bab5f218ff6a9557ff6e9c7c91e8d2ed530..0000000000000000000000000000000000000000 --- a/source/Scrolls/Test.mmt +++ /dev/null @@ -1,28 +0,0 @@ - -/T Miscellaneous scrolls for playing around/testing that don't have a good home yet ⚠-namespace http://mathhub.info/FrameIT/frameworld ⚠-fixmeta ?FrameworldMeta ⚠-theory Test = - meta ?MetaAnnotations?problemTheory ?Test/Problem ♠- meta ?MetaAnnotations?solutionTheory ?Test/Solution ♠- theory Problem = - 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 = - include ?Test/Problem ♠- meta ?MetaAnnotations?label "Test" ♠- meta ?MetaAnnotations?description s"Our Test scroll that given two points ${lverb P} and ${lverb Q} computes the Test of the line ${lverb P Q}." ♠- Test: point - ☠= ⟨0.5 ⋅ (P _x + Q _x), 0.5 ⋅ (P _y + Q _y), 0.5 ⋅ (P _z + Q _z)⟩ - ☠meta ?MetaAnnotations?label s"Mid[${lverb P Q}]" - ☠meta ?MetaAnnotations?description s"The Test between points ${lverb P} and ${lverb Q}." - ♠- ⚠-⚠\ No newline at end of file