From 82552d5f88ae8a4d4d90874c11a12614ceec43be Mon Sep 17 00:00:00 2001 From: Paul-Walcher <paulwalcher12@gmail.com> Date: Sun, 1 Sep 2024 12:27:17 +0200 Subject: [PATCH] cleanup test --- source/MetaTheories.mmt | 2 +- source/Scrolls/Test.mmt | 28 ---------------------------- 2 files changed, 1 insertion(+), 29 deletions(-) delete mode 100644 source/Scrolls/Test.mmt diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt index b4a0122..4bf9b90 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 37049ba..0000000 --- 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 -- GitLab